--- a/src/HOLCF/Lift.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Lift.thy Fri May 08 16:19:51 2009 -0700
@@ -70,11 +70,11 @@
lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R"
by simp
-lemma Def_inject_less_eq: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
-by (simp add: less_lift_def Def_def Abs_lift_inverse lift_def)
+lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
+by (simp add: below_lift_def Def_def Abs_lift_inverse lift_def)
-lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
-by (induct y, simp, simp add: Def_inject_less_eq)
+lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
+by (induct y, simp, simp add: Def_below_Def)
subsection {* Lift is flat *}
@@ -134,7 +134,7 @@
"(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
apply (rule monofunE [where f=flift1])
apply (rule cont2mono [OF cont_flift1])
-apply (simp add: less_fun_ext)
+apply (simp add: below_fun_ext)
done
lemma cont2cont_flift1 [simp]:
@@ -216,7 +216,7 @@
apply (rule is_lubI)
apply (rule ub_rangeI, simp)
apply (drule ub_rangeD)
- apply (erule rev_trans_less)
+ apply (erule rev_below_trans)
apply simp
apply (rule lessI)
done