--- 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;
*}