The commands that set them up as syntax should also set up the standard TeX
override map to do this. For example, boolScript.sml includes the following
lines to set up if-then-else:
val _ = TeX_notation {hol = "if", TeX = ("\\HOLKeyword{if}", 2)}
val _ = TeX_notation {hol = "then", TeX
Seems a good idea to me. Given ETA_AX, it's easy to show equivalence with
current HOL Light, and it's always better to have closed formulae coming out
of definition commands.
One small point: the formulae as written in the linked message do not have
the intended syntactic form (due to bracketing)
Ramana,
On 16 Oct 2014, at 17:18, Ramana Kumar wrote:
> Hi all,
>
> There has been an interesting discussion on the OpenTheory mailing list
> recently regarding how to simplify the two theorems produced by a type
> definition in HOL Light and remove their free variables. The latest message
Hi all,
There has been an interesting discussion on the OpenTheory mailing list
recently regarding how to simplify the two theorems produced by a type
definition in HOL Light and remove their free variables. The latest message
in the thread, which shows the suggestions by Mario Carneiro can be fo
FIRST CALL FOR PAPERS
Thirteenth International Conference on
TYPED LAMBDA CALCULI AND APPLICATIONS (TLCA 2015)
1 July - 3 July 2015, Warsaw, Poland
(co-located with RTA 2015 as part of RDP 2015)
h
CALL FOR WORKSHOPS, TUTORIALS, SYSTEM COMPETITIONS, AND PAPERS
25th International Conference on Automated Deduction (CADE-25)
Berlin, Germany, 1-7 August 2015
http://www.cade-25.info
Submission deadlines:
14 Novemb
