# HG changeset patch
# User huffman
# Date 1118714715 -7200
# Node ID 1ff571813848da29b28793648b2ca5fb3c9cf0b9
# Parent  67f6044c189123e329b7683ed9966efca91fbd16
renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda

diff -r 67f6044c1891 -r 1ff571813848 src/HOLCF/Cont.ML
--- 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";
diff -r 67f6044c1891 -r 1ff571813848 src/HOLCF/Cont.thy
--- 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
diff -r 67f6044c1891 -r 1ff571813848 src/HOLCF/Fix.thy
--- 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]
diff -r 67f6044c1891 -r 1ff571813848 src/HOLCF/Lift.ML
--- 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";
diff -r 67f6044c1891 -r 1ff571813848 src/HOLCF/Lift.thy
--- 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 {*