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