equal
deleted
inserted
replaced
35 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" |
35 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" |
36 token category instead. |
36 token category instead. |
37 |
37 |
38 |
38 |
39 *** HOL *** |
39 *** HOL *** |
|
40 |
|
41 * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1 |
|
42 Minor INCOMPATIBILITY. |
40 |
43 |
41 * Bootstrap of listsum as special case of abstract product over lists. |
44 * Bootstrap of listsum as special case of abstract product over lists. |
42 Fact rename: |
45 Fact rename: |
43 listsum_def ~> listsum.eq_foldr |
46 listsum_def ~> listsum.eq_foldr |
44 INCOMPATIBILITY. |
47 INCOMPATIBILITY. |