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