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 