equal
deleted
inserted
replaced
163 Florian Kammüller; |
163 Florian Kammüller; |
164 |
164 |
165 * HOL: got rid of some global declarations (potential INCOMPATIBILITY |
165 * HOL: got rid of some global declarations (potential INCOMPATIBILITY |
166 for ML tools): const "()" renamed "Product_Type.Unity", type "unit" |
166 for ML tools): const "()" renamed "Product_Type.Unity", type "unit" |
167 renamed "Product_Type.unit"; |
167 renamed "Product_Type.unit"; |
|
168 |
|
169 |
|
170 *** HOLCF *** |
|
171 |
|
172 * proper rep_datatype lift (see theory Lift); use plain induct_tac |
|
173 instead of lift.induct_tac, use UU instead of Undef in all cases; |
168 |
174 |
169 |
175 |
170 *** ZF *** |
176 *** ZF *** |
171 |
177 |
172 * ZF: the integer library now covers quotients and remainders, with |
178 * ZF: the integer library now covers quotients and remainders, with |