# HG changeset patch
# User huffman
# Date 1120783324 -7200
# Node ID fd02f9d06e43ac6451035f5a4b16a2794a5f58ae
# Parent  1b979f8b7e8e336e12f17af7aa19848161a2a9c7
renamed upE1 to upE; added simp rule cont2cont_flift1

diff -r 1b979f8b7e8e -r fd02f9d06e43 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Fri Jul 08 02:41:35 2005 +0200
+++ b/src/HOLCF/Lift.thy	Fri Jul 08 02:42:04 2005 +0200
@@ -33,7 +33,7 @@
 
 lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y"
 apply (induct y)
-apply (rule_tac p=y in upE1)
+apply (rule_tac p=y in upE)
 apply (simp add: Abs_lift_strict)
 apply (case_tac x)
 apply (simp add: Def_def)
@@ -198,6 +198,7 @@
 *}
 
 lemmas cont_lemmas_ext [simp] =
+  cont2cont_flift1
   cont_flift1_arg_and_not_arg cont2cont_lambda
   cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
 
@@ -209,7 +210,7 @@
 
 local val flift1_def = thm "flift1_def"
 in fun cont_tacRs i =
-  simp_tac (simpset() addsimps [flift1_def]) i THEN
+  simp_tac (simpset() (* addsimps [flift1_def] *)) i THEN
   REPEAT (cont_tac i)
 end;
 *}