equal
deleted
inserted
replaced
131 * HOL/recdef (TFL): requires theory Recdef; 'congs' syntax now expects |
131 * HOL/recdef (TFL): requires theory Recdef; 'congs' syntax now expects |
132 comma separated list of theorem names rather than an ML expression; |
132 comma separated list of theorem names rather than an ML expression; |
133 |
133 |
134 * reset HOL_quantifiers by default, i.e. quantifiers are printed as |
134 * reset HOL_quantifiers by default, i.e. quantifiers are printed as |
135 ALL/EX rather than !/?; |
135 ALL/EX rather than !/?; |
|
136 |
|
137 |
|
138 *** LK *** |
|
139 |
|
140 * the notation <<...>> is now available as a notation for sequences of formulas |
|
141 |
|
142 * the simplifier is now installed |
|
143 |
|
144 * the axiom system has been generalized (thanks to Soren Heilmann) |
|
145 |
|
146 * the classical reasoner now has a default rule database |
136 |
147 |
137 |
148 |
138 *** ZF *** |
149 *** ZF *** |
139 |
150 |
140 * new primrec section allows primitive recursive functions to be given |
151 * new primrec section allows primitive recursive functions to be given |