HOLCF: proper rep_datatype lift (see theory Lift); use plain induct_tac
instead of lift.induct_tac, use UU instead of Undef in cases;
--- 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