Use Theory syntax #1109
Description
Seems like there is discussion of adding new syntax to HOL4, see HOL-Theorem-Prover/HOL#1364. If that feature gets added, we probably want to use it.
{{ message }}
Use
Theory syntax #1109Seems like there is discussion of adding new syntax to HOL4, see HOL-Theorem-Prover/HOL#1364. If that feature gets added, we probably want to use it.