equal
deleted
inserted
replaced
39 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" |
39 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" |
40 token category instead. |
40 token category instead. |
41 |
41 |
42 |
42 |
43 *** HOL *** |
43 *** HOL *** |
|
44 |
|
45 * More foundational definition for predicate "even": |
|
46 even_def ~> even_iff_mod_2_eq_zero |
|
47 Minor INCOMPATIBILITY. |
44 |
48 |
45 * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1 |
49 * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1 |
46 Minor INCOMPATIBILITY. |
50 Minor INCOMPATIBILITY. |
47 |
51 |
48 * Bootstrap of listsum as special case of abstract product over lists. |
52 * Bootstrap of listsum as special case of abstract product over lists. |