equal
deleted
inserted
replaced
180 |
180 |
181 - replace "#nnn" by "nnn", and "#-nnn" by "-nnn"; |
181 - replace "#nnn" by "nnn", and "#-nnn" by "-nnn"; |
182 |
182 |
183 - remove all special provisions on numerals in proofs; |
183 - remove all special provisions on numerals in proofs; |
184 |
184 |
|
185 * HOL: symbolic syntax for x^2 (numeral 2); |
|
186 |
185 * HOL: the class of all HOL types is now called "type" rather than |
187 * HOL: the class of all HOL types is now called "type" rather than |
186 "term"; INCOMPATIBILITY, need to adapt references to this type class |
188 "term"; INCOMPATIBILITY, need to adapt references to this type class |
187 in axclass/classes, instance/arities, and (usually rare) occurrences |
189 in axclass/classes, instance/arities, and (usually rare) occurrences |
188 in typings (of consts etc.); internally the class is called |
190 in typings (of consts etc.); internally the class is called |
189 "HOL.type", ML programs should refer to HOLogic.typeS; |
191 "HOL.type", ML programs should refer to HOLogic.typeS; |