equal
deleted
inserted
replaced
19 * HOL: removed duplicate thms in Arith: |
19 * HOL: removed duplicate thms in Arith: |
20 less_imp_add_less should be replaced by trans_less_add1 |
20 less_imp_add_less should be replaced by trans_less_add1 |
21 le_imp_add_le should be replaced by trans_le_add1 |
21 le_imp_add_le should be replaced by trans_le_add1 |
22 |
22 |
23 * HOL: unary - is now overloaded (new type constraints may be required); |
23 * HOL: unary - is now overloaded (new type constraints may be required); |
|
24 |
|
25 * HOL and ZF: unary minus for integers is now #- instead of #~. In ZF, |
|
26 expressions such as n#-1 must be changed to n#- 1, since #-1 is now taken |
|
27 as an integer constant. |
24 |
28 |
25 * Pure: ML function 'theory_of' replaced by 'theory'; |
29 * Pure: ML function 'theory_of' replaced by 'theory'; |
26 |
30 |
27 |
31 |
28 *** Proof tools *** |
32 *** Proof tools *** |