NEWS
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