equal
deleted
inserted
replaced
61 names, so all of the above "constant" names would coincide. Recall |
61 names, so all of the above "constant" names would coincide. Recall |
62 that 'print_syntax' and ML_command "set Syntax.trace_ast" help to |
62 that 'print_syntax' and ML_command "set Syntax.trace_ast" help to |
63 diagnose syntax problems. |
63 diagnose syntax problems. |
64 |
64 |
65 * Type constructors admit general mixfix syntax, not just infix. |
65 * Type constructors admit general mixfix syntax, not just infix. |
|
66 |
|
67 * Concrete syntax may be attached to local entities without a proof |
|
68 body, too. This works via regular mixfix annotations for 'fix', |
|
69 'def', 'obtain' etc. or via the explicit 'write' command, which is |
|
70 similar to the 'notation' command in theory specifications. |
66 |
71 |
67 * Use of cumulative prems via "!" in some proof methods has been |
72 * Use of cumulative prems via "!" in some proof methods has been |
68 discontinued (legacy feature). |
73 discontinued (legacy feature). |
69 |
74 |
70 * References 'trace_simp' and 'debug_simp' have been replaced by |
75 * References 'trace_simp' and 'debug_simp' have been replaced by |
7002 |
7007 |
7003 * 'subtype' facility in HOL for introducing new types as subsets of existing |
7008 * 'subtype' facility in HOL for introducing new types as subsets of existing |
7004 types; |
7009 types; |
7005 |
7010 |
7006 :mode=text:wrap=hard:maxLineLen=72: |
7011 :mode=text:wrap=hard:maxLineLen=72: |
|
7012 |
|
7013 LocalWords: def |