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