# HG changeset patch
# User wenzelm
# Date 1004747613 -3600
# Node ID 9c3377b133c06c89542112033e2a76e46882fea8
# Parent  8809efda06d324c1e4493493255cbd8304f69edc
HOLCF: proper rep_datatype lift (see theory Lift); use plain induct_tac
instead of lift.induct_tac, use UU instead of Undef in cases;

diff -r 8809efda06d3 -r 9c3377b133c0 NEWS
--- 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