equal
deleted
inserted
replaced
73 * Simplified 'typedef' specifications: historical options for implicit |
73 * Simplified 'typedef' specifications: historical options for implicit |
74 set definition and alternative name have been discontinued. The |
74 set definition and alternative name have been discontinued. The |
75 former behavior of "typedef (open) t = A" is now the default, but |
75 former behavior of "typedef (open) t = A" is now the default, but |
76 written just "typedef t = A". INCOMPATIBILITY, need to adapt theories |
76 written just "typedef t = A". INCOMPATIBILITY, need to adapt theories |
77 accordingly. |
77 accordingly. |
78 |
|
79 |
78 |
80 * Theory "Library/Multiset": |
79 * Theory "Library/Multiset": |
81 |
80 |
82 - Renamed constants |
81 - Renamed constants |
83 fold_mset ~> Multiset.fold -- for coherence with other fold combinators |
82 fold_mset ~> Multiset.fold -- for coherence with other fold combinators |
139 less_eq_list.drop ~> less_eq_list_drop |
138 less_eq_list.drop ~> less_eq_list_drop |
140 less_eq_list.induct ~> less_eq_list_induct |
139 less_eq_list.induct ~> less_eq_list_induct |
141 not_le_list_length ~> Sublist.not_sub_length |
140 not_le_list_length ~> Sublist.not_sub_length |
142 |
141 |
143 INCOMPATIBILITY. |
142 INCOMPATIBILITY. |
|
143 |
|
144 * HOL/Rings: renamed lemmas |
|
145 |
|
146 left_distrib ~> distrib_right |
|
147 right_distrib ~> distrib_left |
|
148 |
|
149 in class semiring. INCOMPATIBILITY. |
144 |
150 |
145 * HOL/BNF: New (co)datatype package based on bounded natural |
151 * HOL/BNF: New (co)datatype package based on bounded natural |
146 functors with support for mixed, nested recursion and interesting |
152 functors with support for mixed, nested recursion and interesting |
147 non-free datatypes. |
153 non-free datatypes. |
148 |
154 |