--- a/src/HOLCF/Cont.ML Tue Jun 14 04:04:09 2005 +0200
+++ b/src/HOLCF/Cont.ML Tue Jun 14 04:05:15 2005 +0200
@@ -24,6 +24,7 @@
val cont2cont_CF1L = thm "cont2cont_CF1L";
val mono2mono_MF1L_rev = thm "mono2mono_MF1L_rev";
val cont2cont_CF1L_rev = thm "cont2cont_CF1L_rev";
+val cont2cont_lambda = thm "cont2cont_lambda";
val contlub_abstraction = thm "contlub_abstraction";
val mono2mono_app = thm "mono2mono_app";
val cont2contlub_app = thm "cont2contlub_app";
--- a/src/HOLCF/Cont.thy Tue Jun 14 04:04:09 2005 +0200
+++ b/src/HOLCF/Cont.thy Tue Jun 14 04:05:15 2005 +0200
@@ -235,7 +235,7 @@
apply (blast dest: cont2contlub [THEN contlubE])
done
-lemma cont2cont_CF1L_rev2: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont f"
+lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x y. f x y)"
apply (rule cont2cont_CF1L_rev)
apply simp
done
--- a/src/HOLCF/Fix.thy Tue Jun 14 04:04:09 2005 +0200
+++ b/src/HOLCF/Fix.thy Tue Jun 14 04:05:15 2005 +0200
@@ -100,7 +100,7 @@
by (induct_tac n, simp_all)
lemma cont_iterate: "cont (iterate n)"
-by (rule cont_iterate1 [THEN cont2cont_CF1L_rev2])
+by (rule cont_iterate1 [THEN cont2cont_lambda])
lemmas monofun_iterate2 = cont_iterate2 [THEN cont2mono, standard]
lemmas contlub_iterate2 = cont_iterate2 [THEN cont2contlub, standard]
--- a/src/HOLCF/Lift.ML Tue Jun 14 04:04:09 2005 +0200
+++ b/src/HOLCF/Lift.ML Tue Jun 14 04:05:15 2005 +0200
@@ -24,7 +24,6 @@
val Lift_exhaust = thm "Lift_exhaust";
val UU_lift_def = thm "UU_lift_def";
val Undef_eq_UU = thm "Undef_eq_UU";
-val cont2cont_CF1L_rev2 = thm "cont2cont_CF1L_rev2";
val cont_Rep_CFun_app = thm "cont_Rep_CFun_app";
val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app";
val cont_flift1_arg = thm "cont_flift1_arg";
--- a/src/HOLCF/Lift.thy Tue Jun 14 04:04:09 2005 +0200
+++ b/src/HOLCF/Lift.thy Tue Jun 14 04:05:15 2005 +0200
@@ -265,7 +265,7 @@
lemmas cont_lemmas_ext [simp] =
cont_flift1_arg cont_flift2_arg
- cont_flift1_arg_and_not_arg cont2cont_CF1L_rev2
+ cont_flift1_arg_and_not_arg cont2cont_lambda
cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
ML {*