#
044d704c |
|
22-Jul-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Thm.ETA_CONV -> Drule.ETA_CONV, Thm.Eta -> Drule.RIGHT_ETA Cursory profiling indicates that an implementation of ETA_CONV as a primitive inference rule in Thm is about 20 times faster than an implementation as a derived rule that instantiates ETA_AX, but that the difference in overall HOL build time is negligible. Please do let me know if you encounter (performance) problems due to this change.
|
#
a4c199c6 |
|
13-Dec-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Huge number of check-ins, implementing change to .doc file syntax. Now the rule for text within braces is that it appears as given, but that braces must balance. If you want an unbalanced brace, you can use \lbrace or \rbrace. No existing .doc file uses unbalanced braces. Also, there is now no need to use \noindent. In fact, doing so will get you a complaint from the parser. Similarly, use of \ or {} characters outside of verbatim text blocks will cause griping. All of the new files have been generated by a parse-then-print process from the old files, and it's possible there are errors. If you ever have a spare moment, casting your eye over a random selection of these might help to find errors.
|