changeset 12022 | 9c3377b133c0 |
parent 11995 | 4a622f5fb164 |
child 12034 | 4471077c4d4f |
--- a/NEWS Fri Nov 02 22:02:41 2001 +0100 +++ b/NEWS Sat Nov 03 01:33:33 2001 +0100 @@ -167,6 +167,12 @@ renamed "Product_Type.unit"; +*** HOLCF *** + +* proper rep_datatype lift (see theory Lift); use plain induct_tac +instead of lift.induct_tac, use UU instead of Undef in all cases; + + *** ZF *** * ZF: the integer library now covers quotients and remainders, with