equal
deleted
inserted
replaced
182 
182 
183  replace "#nnn" by "nnn", and "#nnn" by "nnn"; 
183  replace "#nnn" by "nnn", and "#nnn" by "nnn"; 
184 
184 
185  remove all special provisions on numerals in proofs; 
185  remove all special provisions on numerals in proofs; 
186 
186 

187 * HOL: simp rules nat_number_of expand numerals on nat to Suc/0 

188 representation (depends on bin_arith_simps in the default context); 

189 
187 * HOL: symbolic syntax for x^2 (numeral 2); 
190 * HOL: symbolic syntax for x^2 (numeral 2); 
188 
191 
189 * HOL: the class of all HOL types is now called "type" rather than 
192 * HOL: the class of all HOL types is now called "type" rather than 
190 "term"; INCOMPATIBILITY, need to adapt references to this type class 
193 "term"; INCOMPATIBILITY, need to adapt references to this type class 
191 in axclass/classes, instance/arities, and (usually rare) occurrences 
194 in axclass/classes, instance/arities, and (usually rare) occurrences 