equal
deleted
inserted
replaced
55 names, so all of the above "constant" names would coincide. Recall |
55 names, so all of the above "constant" names would coincide. Recall |
56 that 'print_syntax' and ML_command "set Syntax.trace_ast" help to |
56 that 'print_syntax' and ML_command "set Syntax.trace_ast" help to |
57 diagnose syntax problems. |
57 diagnose syntax problems. |
58 |
58 |
59 * Type constructors admit general mixfix syntax, not just infix. |
59 * Type constructors admit general mixfix syntax, not just infix. |
|
60 |
|
61 * Use of cumulative prems via "!" in some proof methods has been |
|
62 discontinued (legacy feature). |
60 |
63 |
61 |
64 |
62 *** Pure *** |
65 *** Pure *** |
63 |
66 |
64 * Code generator: details of internal data cache have no impact on |
67 * Code generator: details of internal data cache have no impact on |