equal
deleted
inserted
replaced
11 recover the old behaviour (e.g. to prevent n+n rewriting to #2*n) |
11 recover the old behaviour (e.g. to prevent n+n rewriting to #2*n) |
12 issue the following ML commands: |
12 issue the following ML commands: |
13 |
13 |
14 Delsimprocs Nat_Numeral_Simprocs.cancel_numerals; |
14 Delsimprocs Nat_Numeral_Simprocs.cancel_numerals; |
15 Delsimprocs [Nat_Numeral_Simprocs.combine_numerals]; |
15 Delsimprocs [Nat_Numeral_Simprocs.combine_numerals]; |
|
16 |
|
17 * HOL: 0 is now overloaded, so the type constraint ::nat may sometimes be |
|
18 needed; |
16 |
19 |
17 * HOL: the constant for f``x is now "image" rather than "op ``"; |
20 * HOL: the constant for f``x is now "image" rather than "op ``"; |
18 |
21 |
19 * HOL: the cartesian product is now "<*>" instead of "Times"; the |
22 * HOL: the cartesian product is now "<*>" instead of "Times"; the |
20 lexicographic product is now "<*lex*>" instead of "**"; |
23 lexicographic product is now "<*lex*>" instead of "**"; |
133 * HOL/ex/Multiquote: multiple nested quotations and anti-quotations -- |
136 * HOL/ex/Multiquote: multiple nested quotations and anti-quotations -- |
134 basically a generalized version of de-Bruijn representation; very |
137 basically a generalized version of de-Bruijn representation; very |
135 useful in avoiding lifting all operations; |
138 useful in avoiding lifting all operations; |
136 |
139 |
137 * HOL/Real: "rabs" replaced by overloaded "abs" function; |
140 * HOL/Real: "rabs" replaced by overloaded "abs" function; |
|
141 |
|
142 * HOL: 0 is now overloaded over the new sort "zero", allowing its use with |
|
143 other numeric types and also as the identity of groups, rings, etc.; |
|
144 |
|
145 * HOL: new axclass plus_ac0 for addition with the AC-laws and 0 as identity. |
|
146 Types nat and int belong to this axclass; |
138 |
147 |
139 * greatly improved simplification involving numerals of type nat & int, e.g. |
148 * greatly improved simplification involving numerals of type nat & int, e.g. |
140 (i + #8 + j) = Suc k simplifies to #7 + (i + j) = k |
149 (i + #8 + j) = Suc k simplifies to #7 + (i + j) = k |
141 i*j + k + j*#3*i simplifies to #4*(i*j) + k |
150 i*j + k + j*#3*i simplifies to #4*(i*j) + k |
142 two terms #m*u and #n*u are replaced by #(m+n)*u |
151 two terms #m*u and #n*u are replaced by #(m+n)*u |