# HG changeset patch
# User huffman
# Date 1241824791 25200
# Node ID 99fe356cbbc2716dfdaed5a8756812f97a8a7805
# Parent  a9d6cf6de9a8f1b4a9fb3bc64293e9f85cd602c9
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names

diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Adm.thy	Fri May 08 16:19:51 2009 -0700
@@ -78,7 +78,7 @@
   "\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> 
     (\<Squnion>i. Y i) = (\<Squnion>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
  apply (frule (1) adm_disj_lemma1)
- apply (rule antisym_less)
+ apply (rule below_antisym)
   apply (rule lub_mono, assumption+)
   apply (erule chain_mono)
   apply (simp add: adm_disj_lemma2)
@@ -122,7 +122,7 @@
 
 text {* admissibility and continuity *}
 
-lemma adm_less: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
+lemma adm_below: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
 apply (rule admI)
 apply (simp add: cont2contlubE)
 apply (rule lub_mono)
@@ -132,7 +132,7 @@
 done
 
 lemma adm_eq: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
-by (simp add: po_eq_conv adm_conj adm_less)
+by (simp add: po_eq_conv adm_conj adm_below)
 
 lemma adm_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
 apply (rule admI)
@@ -142,11 +142,11 @@
 apply (erule spec)
 done
 
-lemma adm_not_less: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
+lemma adm_not_below: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
 apply (rule admI)
 apply (drule_tac x=0 in spec)
 apply (erule contrapos_nn)
-apply (erule rev_trans_less)
+apply (erule rev_below_trans)
 apply (erule cont2mono [THEN monofunE])
 apply (erule is_ub_thelub)
 done
@@ -179,21 +179,21 @@
 apply (drule (1) compactD2, simp)
 apply (erule exE, rule_tac x=i in exI)
 apply (rule max_in_chainI)
-apply (rule antisym_less)
+apply (rule below_antisym)
 apply (erule (1) chain_mono)
-apply (erule (1) trans_less [OF is_ub_thelub])
+apply (erule (1) below_trans [OF is_ub_thelub])
 done
 
 text {* admissibility and compactness *}
 
-lemma adm_compact_not_less: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
+lemma adm_compact_not_below: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
 unfolding compact_def by (rule adm_subst)
 
 lemma adm_neq_compact: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
-by (simp add: po_eq_conv adm_imp adm_not_less adm_compact_not_less)
+by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below)
 
 lemma adm_compact_neq: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
-by (simp add: po_eq_conv adm_imp adm_not_less adm_compact_not_less)
+by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below)
 
 lemma compact_UU [simp, intro]: "compact \<bottom>"
 by (rule compactI, simp add: adm_not_free)
@@ -210,7 +210,7 @@
 
 lemmas adm_lemmas [simp] =
   adm_not_free adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
-  adm_less adm_eq adm_not_less
-  adm_compact_not_less adm_compact_neq adm_neq_compact adm_not_UU
+  adm_below adm_eq adm_not_below
+  adm_compact_not_below adm_compact_neq adm_neq_compact adm_not_UU
 
 end
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Algebraic.thy
--- a/src/HOLCF/Algebraic.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Algebraic.thy	Fri May 08 16:19:51 2009 -0700
@@ -33,21 +33,21 @@
 
 locale pre_deflation =
   fixes f :: "'a \<rightarrow> 'a::cpo"
-  assumes less: "\<And>x. f\<cdot>x \<sqsubseteq> x"
+  assumes below: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   assumes finite_range: "finite (range (\<lambda>x. f\<cdot>x))"
 begin
 
-lemma iterate_less: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x"
-by (induct i, simp_all add: trans_less [OF less])
+lemma iterate_below: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x"
+by (induct i, simp_all add: below_trans [OF below])
 
 lemma iterate_fixed: "f\<cdot>x = x \<Longrightarrow> iterate i\<cdot>f\<cdot>x = x"
 by (induct i, simp_all)
 
 lemma antichain_iterate_app: "i \<le> j \<Longrightarrow> iterate j\<cdot>f\<cdot>x \<sqsubseteq> iterate i\<cdot>f\<cdot>x"
 apply (erule le_Suc_induct)
-apply (simp add: less)
-apply (rule refl_less)
-apply (erule (1) trans_less)
+apply (simp add: below)
+apply (rule below_refl)
+apply (erule (1) below_trans)
 done
 
 lemma finite_range_iterate_app: "finite (range (\<lambda>i. iterate i\<cdot>f\<cdot>x))"
@@ -144,7 +144,7 @@
 next
   fix x :: 'a
   show "d\<cdot>x \<sqsubseteq> x"
-    by (rule MOST_d, simp add: iterate_less)
+    by (rule MOST_d, simp add: iterate_below)
 next
   from finite_range
   have "finite {x. f\<cdot>x = x}"
@@ -163,7 +163,7 @@
   interpret d: finite_deflation d by fact
   fix x
   show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
-    by (simp, rule trans_less [OF d.less f])
+    by (simp, rule below_trans [OF d.below f])
   show "finite (range (\<lambda>x. (d oo f)\<cdot>x))"
     by (rule finite_subset [OF _ d.finite_range], auto)
 qed
@@ -185,9 +185,9 @@
     apply safe
     apply (erule subst)
     apply (rule d.idem)
-    apply (rule antisym_less)
+    apply (rule below_antisym)
     apply (rule f)
-    apply (erule subst, rule d.less)
+    apply (erule subst, rule d.below)
     apply simp
     done
 qed
@@ -199,18 +199,17 @@
 typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
 by (fast intro: finite_deflation_approx)
 
-instantiation fin_defl :: (profinite) sq_ord
+instantiation fin_defl :: (profinite) below
 begin
 
-definition
-  sq_le_fin_defl_def:
+definition below_fin_defl_def:
     "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
 
 instance ..
 end
 
 instance fin_defl :: (profinite) po
-by (rule typedef_po [OF type_definition_fin_defl sq_le_fin_defl_def])
+by (rule typedef_po [OF type_definition_fin_defl below_fin_defl_def])
 
 lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
 using Rep_fin_defl by simp
@@ -218,27 +217,27 @@
 interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
 by (rule finite_deflation_Rep_fin_defl)
 
-lemma fin_defl_lessI:
+lemma fin_defl_belowI:
   "(\<And>x. Rep_fin_defl a\<cdot>x = x \<Longrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a \<sqsubseteq> b"
-unfolding sq_le_fin_defl_def
-by (rule Rep_fin_defl.lessI)
+unfolding below_fin_defl_def
+by (rule Rep_fin_defl.belowI)
 
-lemma fin_defl_lessD:
+lemma fin_defl_belowD:
   "\<lbrakk>a \<sqsubseteq> b; Rep_fin_defl a\<cdot>x = x\<rbrakk> \<Longrightarrow> Rep_fin_defl b\<cdot>x = x"
-unfolding sq_le_fin_defl_def
-by (rule Rep_fin_defl.lessD)
+unfolding below_fin_defl_def
+by (rule Rep_fin_defl.belowD)
 
 lemma fin_defl_eqI:
   "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b"
-apply (rule antisym_less)
-apply (rule fin_defl_lessI, simp)
-apply (rule fin_defl_lessI, simp)
+apply (rule below_antisym)
+apply (rule fin_defl_belowI, simp)
+apply (rule fin_defl_belowI, simp)
 done
 
 lemma Abs_fin_defl_mono:
   "\<lbrakk>finite_deflation a; finite_deflation b; a \<sqsubseteq> b\<rbrakk>
     \<Longrightarrow> Abs_fin_defl a \<sqsubseteq> Abs_fin_defl b"
-unfolding sq_le_fin_defl_def
+unfolding below_fin_defl_def
 by (simp add: Abs_fin_defl_inverse)
 
 
@@ -257,7 +256,7 @@
 apply (rule pre_deflation.finite_deflation_d)
 apply (rule pre_deflation_d_f)
 apply (rule finite_deflation_approx)
-apply (rule Rep_fin_defl.less)
+apply (rule Rep_fin_defl.below)
 done
 
 lemma fd_take_fixed_iff:
@@ -265,10 +264,10 @@
     approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
 unfolding Rep_fin_defl_fd_take
 by (rule eventual_iterate_oo_fixed_iff
-    [OF finite_deflation_approx Rep_fin_defl.less])
+    [OF finite_deflation_approx Rep_fin_defl.below])
 
-lemma fd_take_less: "fd_take n d \<sqsubseteq> d"
-apply (rule fin_defl_lessI)
+lemma fd_take_below: "fd_take n d \<sqsubseteq> d"
+apply (rule fin_defl_belowI)
 apply (simp add: fd_take_fixed_iff)
 done
 
@@ -278,16 +277,16 @@
 done
 
 lemma fd_take_mono: "a \<sqsubseteq> b \<Longrightarrow> fd_take n a \<sqsubseteq> fd_take n b"
-apply (rule fin_defl_lessI)
+apply (rule fin_defl_belowI)
 apply (simp add: fd_take_fixed_iff)
-apply (simp add: fin_defl_lessD)
+apply (simp add: fin_defl_belowD)
 done
 
 lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> approx j\<cdot>x = x"
 by (erule subst, simp add: min_def)
 
 lemma fd_take_chain: "m \<le> n \<Longrightarrow> fd_take m a \<sqsubseteq> fd_take n a"
-apply (rule fin_defl_lessI)
+apply (rule fin_defl_belowI)
 apply (simp add: fd_take_fixed_iff)
 apply (simp add: approx_fixed_le_lemma)
 done
@@ -304,9 +303,9 @@
 lemma fd_take_covers: "\<exists>n. fd_take n a = a"
 apply (rule_tac x=
   "Max ((\<lambda>x. LEAST n. approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
-apply (rule antisym_less)
-apply (rule fd_take_less)
-apply (rule fin_defl_lessI)
+apply (rule below_antisym)
+apply (rule fd_take_below)
+apply (rule fin_defl_belowI)
 apply (simp add: fd_take_fixed_iff)
 apply (rule approx_fixed_le_lemma)
 apply (rule Max_ge)
@@ -320,9 +319,9 @@
 apply (rule Rep_fin_defl.compact)
 done
 
-interpretation fin_defl: basis_take sq_le fd_take
+interpretation fin_defl: basis_take below fd_take
 apply default
-apply (rule fd_take_less)
+apply (rule fd_take_below)
 apply (rule fd_take_idem)
 apply (erule fd_take_mono)
 apply (rule fd_take_chain, simp)
@@ -333,10 +332,10 @@
 subsection {* Defining algebraic deflations by ideal completion *}
 
 typedef (open) 'a alg_defl =
-  "{S::'a fin_defl set. sq_le.ideal S}"
-by (fast intro: sq_le.ideal_principal)
+  "{S::'a fin_defl set. below.ideal S}"
+by (fast intro: below.ideal_principal)
 
-instantiation alg_defl :: (profinite) sq_ord
+instantiation alg_defl :: (profinite) below
 begin
 
 definition
@@ -346,19 +345,19 @@
 end
 
 instance alg_defl :: (profinite) po
-by (rule sq_le.typedef_ideal_po
-    [OF type_definition_alg_defl sq_le_alg_defl_def])
+by (rule below.typedef_ideal_po
+    [OF type_definition_alg_defl below_alg_defl_def])
 
 instance alg_defl :: (profinite) cpo
-by (rule sq_le.typedef_ideal_cpo
-    [OF type_definition_alg_defl sq_le_alg_defl_def])
+by (rule below.typedef_ideal_cpo
+    [OF type_definition_alg_defl below_alg_defl_def])
 
 lemma Rep_alg_defl_lub:
   "chain Y \<Longrightarrow> Rep_alg_defl (\<Squnion>i. Y i) = (\<Union>i. Rep_alg_defl (Y i))"
-by (rule sq_le.typedef_ideal_rep_contlub
-    [OF type_definition_alg_defl sq_le_alg_defl_def])
+by (rule below.typedef_ideal_rep_contlub
+    [OF type_definition_alg_defl below_alg_defl_def])
 
-lemma ideal_Rep_alg_defl: "sq_le.ideal (Rep_alg_defl xs)"
+lemma ideal_Rep_alg_defl: "below.ideal (Rep_alg_defl xs)"
 by (rule Rep_alg_defl [unfolded mem_Collect_eq])
 
 definition
@@ -368,15 +367,15 @@
 lemma Rep_alg_defl_principal:
   "Rep_alg_defl (alg_defl_principal t) = {u. u \<sqsubseteq> t}"
 unfolding alg_defl_principal_def
-by (simp add: Abs_alg_defl_inverse sq_le.ideal_principal)
+by (simp add: Abs_alg_defl_inverse below.ideal_principal)
 
 interpretation alg_defl:
-  ideal_completion sq_le fd_take alg_defl_principal Rep_alg_defl
+  ideal_completion below fd_take alg_defl_principal Rep_alg_defl
 apply default
 apply (rule ideal_Rep_alg_defl)
 apply (erule Rep_alg_defl_lub)
 apply (rule Rep_alg_defl_principal)
-apply (simp only: sq_le_alg_defl_def)
+apply (simp only: below_alg_defl_def)
 done
 
 text {* Algebraic deflations are pointed *}
@@ -443,7 +442,7 @@
   "cast\<cdot>(alg_defl_principal a) = Rep_fin_defl a"
 unfolding cast_def
 apply (rule alg_defl.basis_fun_principal)
-apply (simp only: sq_le_fin_defl_def)
+apply (simp only: below_fin_defl_def)
 done
 
 lemma deflation_cast: "deflation (cast\<cdot>d)"
@@ -522,10 +521,10 @@
     apply (rule finite_deflation_p_d_e)
     apply (rule finite_deflation_cast)
     apply (rule compact_approx)
-    apply (rule sq_ord_less_eq_trans [OF _ d])
+    apply (rule below_eq_trans [OF _ d])
     apply (rule monofun_cfun_fun)
     apply (rule monofun_cfun_arg)
-    apply (rule approx_less)
+    apply (rule approx_below)
     done
   show "(\<Squnion>i. ?a i) = ID"
     apply (rule ext_cfun, simp)
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Bifinite.thy	Fri May 08 16:19:51 2009 -0700
@@ -19,7 +19,7 @@
 
 class bifinite = profinite + pcpo
 
-lemma approx_less: "approx i\<cdot>x \<sqsubseteq> x"
+lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
 proof -
   have "chain (\<lambda>i. approx i\<cdot>x)" by simp
   hence "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by (rule is_ub_thelub)
@@ -32,7 +32,7 @@
   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
     by (rule approx_idem)
   show "approx i\<cdot>x \<sqsubseteq> x"
-    by (rule approx_less)
+    by (rule approx_below)
   show "finite {x. approx i\<cdot>x = x}"
     by (rule finite_fixes_approx)
 qed
@@ -49,17 +49,17 @@
 by (rule ext_cfun, simp add: contlub_cfun_fun)
 
 lemma approx_strict [simp]: "approx i\<cdot>\<bottom> = \<bottom>"
-by (rule UU_I, rule approx_less)
+by (rule UU_I, rule approx_below)
 
 lemma approx_approx1:
   "i \<le> j \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx i\<cdot>x"
-apply (rule deflation_less_comp1 [OF deflation_approx deflation_approx])
+apply (rule deflation_below_comp1 [OF deflation_approx deflation_approx])
 apply (erule chain_mono [OF chain_approx])
 done
 
 lemma approx_approx2:
   "j \<le> i \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx j\<cdot>x"
-apply (rule deflation_less_comp2 [OF deflation_approx deflation_approx])
+apply (rule deflation_below_comp2 [OF deflation_approx deflation_approx])
 apply (erule chain_mono [OF chain_approx])
 done
 
@@ -99,7 +99,7 @@
   thus "P x" by simp
 qed
 
-lemma profinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
+lemma profinite_below_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp)
 apply (rule lub_mono, simp, simp, simp)
 done
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Cfun.thy	Fri May 08 16:19:51 2009 -0700
@@ -105,19 +105,19 @@
 by (rule typedef_finite_po [OF type_definition_CFun])
 
 instance "->" :: (finite_po, chfin) chfin
-by (rule typedef_chfin [OF type_definition_CFun less_CFun_def])
+by (rule typedef_chfin [OF type_definition_CFun below_CFun_def])
 
 instance "->" :: (cpo, discrete_cpo) discrete_cpo
-by intro_classes (simp add: less_CFun_def Rep_CFun_inject)
+by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
 
 instance "->" :: (cpo, pcpo) pcpo
-by (rule typedef_pcpo [OF type_definition_CFun less_CFun_def UU_CFun])
+by (rule typedef_pcpo [OF type_definition_CFun below_CFun_def UU_CFun])
 
 lemmas Rep_CFun_strict =
-  typedef_Rep_strict [OF type_definition_CFun less_CFun_def UU_CFun]
+  typedef_Rep_strict [OF type_definition_CFun below_CFun_def UU_CFun]
 
 lemmas Abs_CFun_strict =
-  typedef_Abs_strict [OF type_definition_CFun less_CFun_def UU_CFun]
+  typedef_Abs_strict [OF type_definition_CFun below_CFun_def UU_CFun]
 
 text {* function application is strict in its first argument *}
 
@@ -153,11 +153,11 @@
 
 text {* Extensionality wrt. ordering for continuous functions *}
 
-lemma expand_cfun_less: "f \<sqsubseteq> g = (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
-by (simp add: less_CFun_def expand_fun_less)
+lemma expand_cfun_below: "f \<sqsubseteq> g = (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
+by (simp add: below_CFun_def expand_fun_below)
 
-lemma less_cfun_ext: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
-by (simp add: expand_cfun_less)
+lemma below_cfun_ext: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
+by (simp add: expand_cfun_below)
 
 text {* Congruence for continuous function application *}
 
@@ -205,13 +205,13 @@
 text {* monotonicity of application *}
 
 lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
-by (simp add: expand_cfun_less)
+by (simp add: expand_cfun_below)
 
 lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y"
 by (rule monofun_Rep_CFun2 [THEN monofunE])
 
 lemma monofun_cfun: "\<lbrakk>f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>y"
-by (rule trans_less [OF monofun_cfun_fun monofun_cfun_arg])
+by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg])
 
 text {* ch2ch - rules for the type @{typ "'a -> 'b"} *}
 
@@ -230,7 +230,7 @@
 
 lemma ch2ch_LAM [simp]:
   "\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)"
-by (simp add: chain_def expand_cfun_less)
+by (simp add: chain_def expand_cfun_below)
 
 text {* contlub, cont properties of @{term Rep_CFun} in both arguments *}
 
@@ -316,7 +316,7 @@
 lemma cont2mono_LAM:
   "\<lbrakk>\<And>x. cont (\<lambda>y. f x y); \<And>y. monofun (\<lambda>x. f x y)\<rbrakk>
     \<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)"
-  unfolding monofun_def expand_cfun_less by simp
+  unfolding monofun_def expand_cfun_below by simp
 
 text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
 
@@ -365,7 +365,7 @@
 
 lemma semi_monofun_Abs_CFun:
   "\<lbrakk>cont f; cont g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> Abs_CFun f \<sqsubseteq> Abs_CFun g"
-by (simp add: less_CFun_def Abs_CFun_inverse2)
+by (simp add: below_CFun_def Abs_CFun_inverse2)
 
 text {* some lemmata for functions with flat/chfin domain/range types *}
 
@@ -401,7 +401,7 @@
 apply simp
 done
 
-lemma injection_less:
+lemma injection_below:
   "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> (g\<cdot>x \<sqsubseteq> g\<cdot>y) = (x \<sqsubseteq> y)"
 apply (rule iffI)
 apply (drule_tac f=f in monofun_cfun_arg)
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/CompactBasis.thy	Fri May 08 16:19:51 2009 -0700
@@ -18,7 +18,7 @@
 lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
 by (rule Rep_compact_basis [unfolded mem_Collect_eq])
 
-instantiation compact_basis :: (profinite) sq_ord
+instantiation compact_basis :: (profinite) below
 begin
 
 definition
@@ -47,12 +47,12 @@
 lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
 
 interpretation compact_basis:
-  basis_take sq_le compact_take
+  basis_take below compact_take
 proof
   fix n :: nat and a :: "'a compact_basis"
   show "compact_take n a \<sqsubseteq> a"
     unfolding compact_le_def
-    by (simp add: Rep_compact_take approx_less)
+    by (simp add: Rep_compact_take approx_below)
 next
   fix n :: nat and a :: "'a compact_basis"
   show "compact_take n (compact_take n a) = compact_take n a"
@@ -93,15 +93,15 @@
   "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
 
 interpretation compact_basis:
-  ideal_completion sq_le compact_take Rep_compact_basis approximants
+  ideal_completion below compact_take Rep_compact_basis approximants
 proof
   fix w :: 'a
-  show "preorder.ideal sq_le (approximants w)"
-  proof (rule sq_le.idealI)
+  show "preorder.ideal below (approximants w)"
+  proof (rule below.idealI)
     show "\<exists>x. x \<in> approximants w"
       unfolding approximants_def
       apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
-      apply (simp add: Abs_compact_basis_inverse approx_less)
+      apply (simp add: Abs_compact_basis_inverse approx_below)
       done
   next
     fix x y :: "'a compact_basis"
@@ -116,7 +116,7 @@
       apply (clarify, rename_tac i j)
       apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
       apply (simp add: compact_le_def)
-      apply (simp add: Abs_compact_basis_inverse approx_less)
+      apply (simp add: Abs_compact_basis_inverse approx_below)
       apply (erule subst, erule subst)
       apply (simp add: monofun_cfun chain_mono [OF chain_approx])
       done
@@ -126,7 +126,7 @@
       unfolding approximants_def
       apply simp
       apply (simp add: compact_le_def)
-      apply (erule (1) trans_less)
+      apply (erule (1) below_trans)
       done
   qed
 next
@@ -136,7 +136,7 @@
     unfolding approximants_def
     apply safe
     apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
-    apply (erule trans_less, rule is_ub_thelub [OF Y])
+    apply (erule below_trans, rule is_ub_thelub [OF Y])
     done
 next
   fix a :: "'a compact_basis"
@@ -148,7 +148,7 @@
     apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
     apply (rule admD, simp, simp)
     apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
-    apply (simp add: approximants_def Abs_compact_basis_inverse approx_less)
+    apply (simp add: approximants_def Abs_compact_basis_inverse approx_below)
     apply (simp add: approximants_def Abs_compact_basis_inverse)
     done
 qed
@@ -288,7 +288,7 @@
 apply (cut_tac a=a in compact_basis.take_covers)
 apply (clarify, rule_tac x=n in exI)
 apply (clarify, simp)
-apply (rule antisym_less)
+apply (rule below_antisym)
 apply (rule compact_basis.take_less)
 apply (drule_tac a=a in compact_basis.take_chain_le)
 apply simp
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Completion.thy
--- a/src/HOLCF/Completion.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Completion.thy	Fri May 08 16:19:51 2009 -0700
@@ -108,11 +108,11 @@
 done
 
 lemma typedef_ideal_po:
-  fixes Abs :: "'a set \<Rightarrow> 'b::sq_ord"
+  fixes Abs :: "'a set \<Rightarrow> 'b::below"
   assumes type: "type_definition Rep Abs {S. ideal S}"
-  assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
+  assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
   shows "OFCLASS('b, po_class)"
- apply (intro_classes, unfold less)
+ apply (intro_classes, unfold below)
    apply (rule subset_refl)
   apply (erule (1) subset_trans)
  apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
@@ -122,7 +122,7 @@
 lemma
   fixes Abs :: "'a set \<Rightarrow> 'b::po"
   assumes type: "type_definition Rep Abs {S. ideal S}"
-  assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
+  assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
   assumes S: "chain S"
   shows typedef_ideal_lub: "range S <<| Abs (\<Union>i. Rep (S i))"
     and typedef_ideal_rep_contlub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
@@ -130,7 +130,7 @@
   have 1: "ideal (\<Union>i. Rep (S i))"
     apply (rule ideal_UN)
      apply (rule type_definition.Rep [OF type, unfolded mem_Collect_eq])
-    apply (subst less [symmetric])
+    apply (subst below [symmetric])
     apply (erule chain_mono [OF S])
     done
   hence 2: "Rep (Abs (\<Union>i. Rep (S i))) = (\<Union>i. Rep (S i))"
@@ -138,8 +138,8 @@
   show 3: "range S <<| Abs (\<Union>i. Rep (S i))"
     apply (rule is_lubI)
      apply (rule is_ubI)
-     apply (simp add: less 2, fast)
-    apply (simp add: less 2 is_ub_def, fast)
+     apply (simp add: below 2, fast)
+    apply (simp add: below 2 is_ub_def, fast)
     done
   hence 4: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))"
     by (rule thelubI)
@@ -150,16 +150,16 @@
 lemma typedef_ideal_cpo:
   fixes Abs :: "'a set \<Rightarrow> 'b::po"
   assumes type: "type_definition Rep Abs {S. ideal S}"
-  assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
+  assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
   shows "OFCLASS('b, cpo_class)"
-by (default, rule exI, erule typedef_ideal_lub [OF type less])
+by (default, rule exI, erule typedef_ideal_lub [OF type below])
 
 end
 
-interpretation sq_le: preorder "sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
+interpretation below: preorder "below :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
 apply unfold_locales
-apply (rule refl_less)
-apply (erule (1) trans_less)
+apply (rule below_refl)
+apply (erule (1) below_trans)
 done
 
 subsection {* Lemmas about least upper bounds *}
@@ -229,43 +229,43 @@
 apply (rule subsetI, rule UN_I [where a=0], simp_all)
 done
 
-lemma less_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
+lemma below_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
 by (rule iffI [OF rep_mono subset_repD])
 
 lemma rep_eq: "rep x = {a. principal a \<sqsubseteq> x}"
-unfolding less_def rep_principal
+unfolding below_def rep_principal
 apply safe
 apply (erule (1) idealD3 [OF ideal_rep])
 apply (erule subsetD, simp add: r_refl)
 done
 
-lemma mem_rep_iff_principal_less: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
+lemma mem_rep_iff_principal_below: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
 by (simp add: rep_eq)
 
-lemma principal_less_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
+lemma principal_below_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
 by (simp add: rep_eq)
 
-lemma principal_less_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
-by (simp add: principal_less_iff_mem_rep rep_principal)
+lemma principal_below_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
+by (simp add: principal_below_iff_mem_rep rep_principal)
 
 lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> a \<preceq> b \<and> b \<preceq> a"
-unfolding po_eq_conv [where 'a='b] principal_less_iff ..
+unfolding po_eq_conv [where 'a='b] principal_below_iff ..
 
 lemma repD: "a \<in> rep x \<Longrightarrow> principal a \<sqsubseteq> x"
 by (simp add: rep_eq)
 
 lemma principal_mono: "a \<preceq> b \<Longrightarrow> principal a \<sqsubseteq> principal b"
-by (simp only: principal_less_iff)
+by (simp only: principal_below_iff)
 
-lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
-unfolding principal_less_iff_mem_rep
-by (simp add: less_def subset_eq)
+lemma belowI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
+unfolding principal_below_iff_mem_rep
+by (simp add: below_def subset_eq)
 
 lemma lub_principal_rep: "principal ` rep x <<| x"
 apply (rule is_lubI)
 apply (rule ub_imageI)
 apply (erule repD)
-apply (subst less_def)
+apply (subst below_def)
 apply (rule subsetI)
 apply (drule (1) ub_imageD)
 apply (simp add: rep_eq)
@@ -299,7 +299,7 @@
  apply (rule is_lub_thelub0)
   apply (rule basis_fun_lemma0, erule f_mono)
  apply (rule is_ubI, clarsimp, rename_tac a)
- apply (rule trans_less [OF f_mono [OF take_chain]])
+ apply (rule below_trans [OF f_mono [OF take_chain]])
  apply (rule is_ub_thelub0)
   apply (rule basis_fun_lemma0, erule f_mono)
  apply simp
@@ -313,7 +313,7 @@
  apply (rule ub_imageI, rename_tac a)
   apply (cut_tac a=a in take_covers, erule exE, rename_tac i)
   apply (erule subst)
-  apply (rule rev_trans_less)
+  apply (rule rev_below_trans)
    apply (rule_tac x=i in is_ub_thelub)
    apply (rule basis_fun_lemma1, erule f_mono)
   apply (rule is_ub_thelub0)
@@ -324,7 +324,7 @@
  apply (rule is_lub_thelub0)
   apply (rule basis_fun_lemma0, erule f_mono)
  apply (rule is_ubI, clarsimp, rename_tac a)
- apply (rule trans_less [OF f_mono [OF take_less]])
+ apply (rule below_trans [OF f_mono [OF take_less]])
  apply (erule (1) ub_imageD)
 done
 
@@ -350,7 +350,7 @@
      apply (erule (1) subsetD [OF rep_mono])
     apply (rule is_lub_thelub0 [OF lub ub_imageI])
     apply (simp add: rep_contlub, clarify)
-    apply (erule rev_trans_less [OF is_ub_thelub])
+    apply (erule rev_below_trans [OF is_ub_thelub])
     apply (erule is_ub_thelub0 [OF lub imageI])
     done
 qed
@@ -367,21 +367,21 @@
 lemma basis_fun_mono:
   assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b"
-  assumes less: "\<And>a. f a \<sqsubseteq> g a"
+  assumes below: "\<And>a. f a \<sqsubseteq> g a"
   shows "basis_fun f \<sqsubseteq> basis_fun g"
- apply (rule less_cfun_ext)
+ apply (rule below_cfun_ext)
  apply (simp only: basis_fun_beta f_mono g_mono)
  apply (rule is_lub_thelub0)
   apply (rule basis_fun_lemma, erule f_mono)
  apply (rule ub_imageI, rename_tac a)
- apply (rule trans_less [OF less])
+ apply (rule below_trans [OF below])
  apply (rule is_ub_thelub0)
   apply (rule basis_fun_lemma, erule g_mono)
  apply (erule imageI)
 done
 
 lemma compact_principal [simp]: "compact (principal a)"
-by (rule compactI2, simp add: principal_less_iff_mem_rep rep_contlub)
+by (rule compactI2, simp add: principal_below_iff_mem_rep rep_contlub)
 
 subsection {* Bifiniteness of ideal completions *}
 
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Cont.thy	Fri May 08 16:19:51 2009 -0700
@@ -121,14 +121,14 @@
 
 lemma contI2:
   assumes mono: "monofun f"
-  assumes less: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
+  assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
      \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
   shows "cont f"
 apply (rule monocontlub2cont)
 apply (rule mono)
 apply (rule contlubI)
-apply (rule antisym_less)
-apply (rule less, assumption)
+apply (rule below_antisym)
+apply (rule below, assumption)
 apply (erule ch2ch_monofun [OF mono])
 apply (rule is_lub_thelub)
 apply (erule ch2ch_monofun [OF mono])
@@ -192,7 +192,7 @@
     by (auto intro: cont2monofunE [OF 1]
                     cont2monofunE [OF 2]
                     cont2monofunE [OF 3]
-                    trans_less)
+                    below_trans)
 next
   fix Y :: "nat \<Rightarrow> 'a" assume "chain Y"
   then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) = (\<Squnion>i. f (Y i) (t (Y i)))"
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/ConvexPD.thy	Fri May 08 16:19:51 2009 -0700
@@ -144,7 +144,7 @@
   "{S::'a pd_basis set. convex_le.ideal S}"
 by (fast intro: convex_le.ideal_principal)
 
-instantiation convex_pd :: (profinite) sq_ord
+instantiation convex_pd :: (profinite) below
 begin
 
 definition
@@ -155,16 +155,16 @@
 
 instance convex_pd :: (profinite) po
 by (rule convex_le.typedef_ideal_po
-    [OF type_definition_convex_pd sq_le_convex_pd_def])
+    [OF type_definition_convex_pd below_convex_pd_def])
 
 instance convex_pd :: (profinite) cpo
 by (rule convex_le.typedef_ideal_cpo
-    [OF type_definition_convex_pd sq_le_convex_pd_def])
+    [OF type_definition_convex_pd below_convex_pd_def])
 
 lemma Rep_convex_pd_lub:
   "chain Y \<Longrightarrow> Rep_convex_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_convex_pd (Y i))"
 by (rule convex_le.typedef_ideal_rep_contlub
-    [OF type_definition_convex_pd sq_le_convex_pd_def])
+    [OF type_definition_convex_pd below_convex_pd_def])
 
 lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
 by (rule Rep_convex_pd [unfolded mem_Collect_eq])
@@ -190,7 +190,7 @@
 apply (rule ideal_Rep_convex_pd)
 apply (erule Rep_convex_pd_lub)
 apply (rule Rep_convex_principal)
-apply (simp only: sq_le_convex_pd_def)
+apply (simp only: below_convex_pd_def)
 done
 
 text {* Convex powerdomain is pointed *}
@@ -311,7 +311,7 @@
 lemmas convex_plus_aci =
   convex_plus_ac convex_plus_absorb convex_plus_left_absorb
 
-lemma convex_unit_less_plus_iff [simp]:
+lemma convex_unit_below_plus_iff [simp]:
   "{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
  apply (rule iffI)
   apply (subgoal_tac
@@ -329,7 +329,7 @@
  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
 done
 
-lemma convex_plus_less_unit_iff [simp]:
+lemma convex_plus_below_unit_iff [simp]:
   "xs +\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>"
  apply (rule iffI)
   apply (subgoal_tac
@@ -347,9 +347,9 @@
  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
 done
 
-lemma convex_unit_less_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
+lemma convex_unit_below_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
  apply (rule iffI)
-  apply (rule profinite_less_ext)
+  apply (rule profinite_below_ext)
   apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
@@ -433,12 +433,12 @@
 
 lemma monofun_LAM:
   "\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
-by (simp add: expand_cfun_less)
+by (simp add: expand_cfun_below)
 
 lemma convex_bind_basis_mono:
   "t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u"
 apply (erule convex_le_induct)
-apply (erule (1) trans_less)
+apply (erule (1) below_trans)
 apply (simp add: monofun_LAM monofun_cfun)
 apply (simp add: monofun_LAM monofun_cfun)
 done
@@ -606,12 +606,12 @@
 
 text {* Ordering property *}
 
-lemma convex_pd_less_iff:
+lemma convex_pd_below_iff:
   "(xs \<sqsubseteq> ys) =
     (convex_to_upper\<cdot>xs \<sqsubseteq> convex_to_upper\<cdot>ys \<and>
      convex_to_lower\<cdot>xs \<sqsubseteq> convex_to_lower\<cdot>ys)"
  apply (safe elim!: monofun_cfun_arg)
- apply (rule profinite_less_ext)
+ apply (rule profinite_below_ext)
  apply (drule_tac f="approx i" in monofun_cfun_arg)
  apply (drule_tac f="approx i" in monofun_cfun_arg)
  apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp)
@@ -620,19 +620,19 @@
  apply (simp add: approx_convex_to_upper approx_convex_to_lower convex_le_def)
 done
 
-lemmas convex_plus_less_plus_iff =
-  convex_pd_less_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard]
+lemmas convex_plus_below_plus_iff =
+  convex_pd_below_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard]
 
-lemmas convex_pd_less_simps =
-  convex_unit_less_plus_iff
-  convex_plus_less_unit_iff
-  convex_plus_less_plus_iff
-  convex_unit_less_iff
+lemmas convex_pd_below_simps =
+  convex_unit_below_plus_iff
+  convex_plus_below_unit_iff
+  convex_plus_below_plus_iff
+  convex_unit_below_iff
   convex_to_upper_unit
   convex_to_upper_plus
   convex_to_lower_unit
   convex_to_lower_plus
-  upper_pd_less_simps
-  lower_pd_less_simps
+  upper_pd_below_simps
+  lower_pd_below_simps
 
 end
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Cprod.thy	Fri May 08 16:19:51 2009 -0700
@@ -68,7 +68,7 @@
 lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' \<and> b = b')"
 by (simp add: cpair_eq_pair)
 
-lemma cpair_less [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
+lemma cpair_below [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
 by (simp add: cpair_eq_pair)
 
 lemma cpair_defined_iff [iff]: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
@@ -107,23 +107,23 @@
 
 lemmas surjective_pairing_Cprod2 = cpair_cfst_csnd
 
-lemma less_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
-by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd)
+lemma below_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
+by (simp add: below_prod_def cfst_def csnd_def cont_fst cont_snd)
 
 lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
-by (auto simp add: po_eq_conv less_cprod)
+by (auto simp add: po_eq_conv below_cprod)
 
-lemma cfst_less_iff: "cfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <y, csnd\<cdot>x>"
-by (simp add: less_cprod)
+lemma cfst_below_iff: "cfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <y, csnd\<cdot>x>"
+by (simp add: below_cprod)
 
-lemma csnd_less_iff: "csnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <cfst\<cdot>x, y>"
-by (simp add: less_cprod)
+lemma csnd_below_iff: "csnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <cfst\<cdot>x, y>"
+by (simp add: below_cprod)
 
 lemma compact_cfst: "compact x \<Longrightarrow> compact (cfst\<cdot>x)"
-by (rule compactI, simp add: cfst_less_iff)
+by (rule compactI, simp add: cfst_below_iff)
 
 lemma compact_csnd: "compact x \<Longrightarrow> compact (csnd\<cdot>x)"
-by (rule compactI, simp add: csnd_less_iff)
+by (rule compactI, simp add: csnd_below_iff)
 
 lemma compact_cpair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
 by (simp add: cpair_eq_pair)
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Deflation.thy
--- a/src/HOLCF/Deflation.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Deflation.thy	Fri May 08 16:19:51 2009 -0700
@@ -15,11 +15,11 @@
 locale deflation =
   fixes d :: "'a \<rightarrow> 'a"
   assumes idem: "\<And>x. d\<cdot>(d\<cdot>x) = d\<cdot>x"
-  assumes less: "\<And>x. d\<cdot>x \<sqsubseteq> x"
+  assumes below: "\<And>x. d\<cdot>x \<sqsubseteq> x"
 begin
 
-lemma less_ID: "d \<sqsubseteq> ID"
-by (rule less_cfun_ext, simp add: less)
+lemma below_ID: "d \<sqsubseteq> ID"
+by (rule below_cfun_ext, simp add: below)
 
 text {* The set of fixed points is the same as the range. *}
 
@@ -34,18 +34,18 @@
   the subset ordering of their sets of fixed-points.
 *}
 
-lemma lessI:
+lemma belowI:
   assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
-proof (rule less_cfun_ext)
+proof (rule below_cfun_ext)
   fix x
-  from less have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
+  from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
   also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
   finally show "d\<cdot>x \<sqsubseteq> f\<cdot>x" .
 qed
 
-lemma lessD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
-proof (rule antisym_less)
-  from less show "d\<cdot>x \<sqsubseteq> x" .
+lemma belowD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
+proof (rule below_antisym)
+  from below show "d\<cdot>x \<sqsubseteq> x" .
 next
   assume "f \<sqsubseteq> d"
   hence "f\<cdot>x \<sqsubseteq> d\<cdot>x" by (rule monofun_cfun_fun)
@@ -64,11 +64,11 @@
 lemma deflation_UU: "deflation \<bottom>"
 by (simp add: deflation.intro)
 
-lemma deflation_less_iff:
+lemma deflation_below_iff:
   "\<lbrakk>deflation p; deflation q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q \<longleftrightarrow> (\<forall>x. p\<cdot>x = x \<longrightarrow> q\<cdot>x = x)"
  apply safe
-  apply (simp add: deflation.lessD)
- apply (simp add: deflation.lessI)
+  apply (simp add: deflation.belowD)
+ apply (simp add: deflation.belowI)
 done
 
 text {*
@@ -76,13 +76,13 @@
   the lesser of the two (if they are comparable).
 *}
 
-lemma deflation_less_comp1:
+lemma deflation_below_comp1:
   assumes "deflation f"
   assumes "deflation g"
   shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
-proof (rule antisym_less)
+proof (rule below_antisym)
   interpret g: deflation g by fact
-  from g.less show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
+  from g.below show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
 next
   interpret f: deflation f by fact
   assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
@@ -91,9 +91,9 @@
   finally show "f\<cdot>x \<sqsubseteq> f\<cdot>(g\<cdot>x)" .
 qed
 
-lemma deflation_less_comp2:
+lemma deflation_below_comp2:
   "\<lbrakk>deflation f; deflation g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> g\<cdot>(f\<cdot>x) = f\<cdot>x"
-by (simp only: deflation.lessD deflation.idem)
+by (simp only: deflation.belowD deflation.idem)
 
 
 subsection {* Deflations with finite range *}
@@ -143,7 +143,7 @@
   hence "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)"
     using j by simp
   hence "d\<cdot>x \<sqsubseteq> Y j"
-    using less by (rule trans_less)
+    using below by (rule below_trans)
   thus "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" ..
 qed
 
@@ -155,10 +155,10 @@
 locale ep_pair =
   fixes e :: "'a \<rightarrow> 'b" and p :: "'b \<rightarrow> 'a"
   assumes e_inverse [simp]: "\<And>x. p\<cdot>(e\<cdot>x) = x"
-  and e_p_less: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y"
+  and e_p_below: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y"
 begin
 
-lemma e_less_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
+lemma e_below_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
 proof
   assume "e\<cdot>x \<sqsubseteq> e\<cdot>y"
   hence "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>(e\<cdot>y)" by (rule monofun_cfun_arg)
@@ -169,7 +169,7 @@
 qed
 
 lemma e_eq_iff [simp]: "e\<cdot>x = e\<cdot>y \<longleftrightarrow> x = y"
-unfolding po_eq_conv e_less_iff ..
+unfolding po_eq_conv e_below_iff ..
 
 lemma p_eq_iff:
   "\<lbrakk>e\<cdot>(p\<cdot>x) = x; e\<cdot>(p\<cdot>y) = y\<rbrakk> \<Longrightarrow> p\<cdot>x = p\<cdot>y \<longleftrightarrow> x = y"
@@ -178,7 +178,7 @@
 lemma p_inverse: "(\<exists>x. y = e\<cdot>x) = (e\<cdot>(p\<cdot>y) = y)"
 by (auto, rule exI, erule sym)
 
-lemma e_less_iff_less_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
+lemma e_below_iff_below_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
 proof
   assume "e\<cdot>x \<sqsubseteq> y"
   then have "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>y" by (rule monofun_cfun_arg)
@@ -186,7 +186,7 @@
 next
   assume "x \<sqsubseteq> p\<cdot>y"
   then have "e\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>y)" by (rule monofun_cfun_arg)
-  then show "e\<cdot>x \<sqsubseteq> y" using e_p_less by (rule trans_less)
+  then show "e\<cdot>x \<sqsubseteq> y" using e_p_below by (rule below_trans)
 qed
 
 lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
@@ -203,7 +203,7 @@
   assume "compact x"
   hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
   hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
-  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_less_iff_less_p)
+  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_below_iff_below_p)
   thus "compact (e\<cdot>x)" by (rule compactI)
 qed
 
@@ -213,7 +213,7 @@
 text {* Deflations from ep-pairs *}
 
 lemma deflation_e_p: "deflation (e oo p)"
-by (simp add: deflation.intro e_p_less)
+by (simp add: deflation.intro e_p_below)
 
 lemma deflation_e_d_p:
   assumes "deflation d"
@@ -224,7 +224,7 @@
   show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
     by (simp add: idem)
   show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
-    by (simp add: e_less_iff_less_p less)
+    by (simp add: e_below_iff_below_p below)
 qed
 
 lemma finite_deflation_e_d_p:
@@ -236,7 +236,7 @@
   show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
     by (simp add: idem)
   show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
-    by (simp add: e_less_iff_less_p less)
+    by (simp add: e_below_iff_below_p below)
   have "finite ((\<lambda>x. e\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. p\<cdot>x))"
     by (simp add: finite_image)
   hence "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))"
@@ -254,24 +254,24 @@
   {
     fix x
     have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
-      by (rule d.less)
+      by (rule d.below)
     hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(e\<cdot>x)"
       by (rule monofun_cfun_arg)
     hence "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
       by simp
   }
-  note p_d_e_less = this
+  note p_d_e_below = this
   show ?thesis
   proof
     fix x
     show "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
-      by (rule p_d_e_less)
+      by (rule p_d_e_below)
   next
     fix x
     show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) = (p oo d oo e)\<cdot>x"
-    proof (rule antisym_less)
+    proof (rule below_antisym)
       show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) \<sqsubseteq> (p oo d oo e)\<cdot>x"
-        by (rule p_d_e_less)
+        by (rule p_d_e_below)
       have "p\<cdot>(d\<cdot>(d\<cdot>(d\<cdot>(e\<cdot>x)))) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
         by (intro monofun_cfun_arg d)
       hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
@@ -315,29 +315,29 @@
 lemma ep_pair_unique_e_lemma:
   assumes "ep_pair e1 p" and "ep_pair e2 p"
   shows "e1 \<sqsubseteq> e2"
-proof (rule less_cfun_ext)
+proof (rule below_cfun_ext)
   interpret e1: ep_pair e1 p by fact
   interpret e2: ep_pair e2 p by fact
   fix x
   have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
-    by (rule e1.e_p_less)
+    by (rule e1.e_p_below)
   thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
     by (simp only: e2.e_inverse)
 qed
 
 lemma ep_pair_unique_e:
   "\<lbrakk>ep_pair e1 p; ep_pair e2 p\<rbrakk> \<Longrightarrow> e1 = e2"
-by (fast intro: antisym_less elim: ep_pair_unique_e_lemma)
+by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
 
 lemma ep_pair_unique_p_lemma:
   assumes "ep_pair e p1" and "ep_pair e p2"
   shows "p1 \<sqsubseteq> p2"
-proof (rule less_cfun_ext)
+proof (rule below_cfun_ext)
   interpret p1: ep_pair e p1 by fact
   interpret p2: ep_pair e p2 by fact
   fix x
   have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
-    by (rule p1.e_p_less)
+    by (rule p1.e_p_below)
   hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
     by (rule monofun_cfun_arg)
   thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
@@ -346,7 +346,7 @@
 
 lemma ep_pair_unique_p:
   "\<lbrakk>ep_pair e p1; ep_pair e p2\<rbrakk> \<Longrightarrow> p1 = p2"
-by (fast intro: antisym_less elim: ep_pair_unique_p_lemma)
+by (fast intro: below_antisym elim: ep_pair_unique_p_lemma)
 
 subsection {* Composing ep-pairs *}
 
@@ -363,11 +363,11 @@
   show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x"
     by simp
   have "e1\<cdot>(p1\<cdot>(p2\<cdot>y)) \<sqsubseteq> p2\<cdot>y"
-    by (rule ep1.e_p_less)
+    by (rule ep1.e_p_below)
   hence "e2\<cdot>(e1\<cdot>(p1\<cdot>(p2\<cdot>y))) \<sqsubseteq> e2\<cdot>(p2\<cdot>y)"
     by (rule monofun_cfun_arg)
   also have "e2\<cdot>(p2\<cdot>y) \<sqsubseteq> y"
-    by (rule ep2.e_p_less)
+    by (rule ep2.e_p_below)
   finally show "(e2 oo e1)\<cdot>((p1 oo p2)\<cdot>y) \<sqsubseteq> y"
     by simp
 qed
@@ -381,7 +381,7 @@
 proof -
   have "\<bottom> \<sqsubseteq> p\<cdot>\<bottom>" by (rule minimal)
   hence "e\<cdot>\<bottom> \<sqsubseteq> e\<cdot>(p\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
-  also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_less)
+  also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_below)
   finally show "e\<cdot>\<bottom> = \<bottom>" by simp
 qed
 
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Discrete.thy
--- a/src/HOLCF/Discrete.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Discrete.thy	Fri May 08 16:19:51 2009 -0700
@@ -12,21 +12,21 @@
 
 subsection {* Type @{typ "'a discr"} is a discrete cpo *}
 
-instantiation discr :: (type) sq_ord
+instantiation discr :: (type) below
 begin
 
 definition
-  less_discr_def:
+  below_discr_def:
     "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
 
 instance ..
 end
 
 instance discr :: (type) discrete_cpo
-by intro_classes (simp add: less_discr_def)
+by intro_classes (simp add: below_discr_def)
 
-lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
-by simp
+lemma discr_below_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
+by simp (* FIXME: same discrete_cpo - remove? is [iff] important? *)
 
 subsection {* Type @{typ "'a discr"} is a cpo *}
 
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Domain.thy	Fri May 08 16:19:51 2009 -0700
@@ -33,7 +33,7 @@
 lemma swap: "iso rep abs"
   by (rule iso.intro [OF rep_iso abs_iso])
 
-lemma abs_less: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"
+lemma abs_below: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"
 proof
   assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y"
   then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg)
@@ -43,11 +43,11 @@
   then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg)
 qed
 
-lemma rep_less: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"
-  by (rule iso.abs_less [OF swap])
+lemma rep_below: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"
+  by (rule iso.abs_below [OF swap])
 
 lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)"
-  by (simp add: po_eq_conv abs_less)
+  by (simp add: po_eq_conv abs_below)
 
 lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)"
   by (rule iso.abs_eq [OF swap])
@@ -91,7 +91,7 @@
   assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
   with cont_Rep_CFun2
   have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
-  then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_less by simp
+  then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp
 qed
 
 lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Ffun.thy
--- a/src/HOLCF/Ffun.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Ffun.thy	Fri May 08 16:19:51 2009 -0700
@@ -10,11 +10,11 @@
 
 subsection {* Full function space is a partial order *}
 
-instantiation "fun"  :: (type, sq_ord) sq_ord
+instantiation "fun"  :: (type, below) below
 begin
 
 definition
-  less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"  
+  below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
 
 instance ..
 end
@@ -23,45 +23,45 @@
 proof
   fix f :: "'a \<Rightarrow> 'b"
   show "f \<sqsubseteq> f"
-    by (simp add: less_fun_def)
+    by (simp add: below_fun_def)
 next
   fix f g :: "'a \<Rightarrow> 'b"
   assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
-    by (simp add: less_fun_def expand_fun_eq antisym_less)
+    by (simp add: below_fun_def expand_fun_eq below_antisym)
 next
   fix f g h :: "'a \<Rightarrow> 'b"
   assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
-    unfolding less_fun_def by (fast elim: trans_less)
+    unfolding below_fun_def by (fast elim: below_trans)
 qed
 
 text {* make the symbol @{text "<<"} accessible for type fun *}
 
-lemma expand_fun_less: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
-by (simp add: less_fun_def)
+lemma expand_fun_below: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
+by (simp add: below_fun_def)
 
-lemma less_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
-by (simp add: less_fun_def)
+lemma below_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
+by (simp add: below_fun_def)
 
 subsection {* Full function space is chain complete *}
 
 text {* function application is monotone *}
 
 lemma monofun_app: "monofun (\<lambda>f. f x)"
-by (rule monofunI, simp add: less_fun_def)
+by (rule monofunI, simp add: below_fun_def)
 
 text {* chains of functions yield chains in the po range *}
 
 lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
-by (simp add: chain_def less_fun_def)
+by (simp add: chain_def below_fun_def)
 
 lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
-by (simp add: chain_def less_fun_def)
+by (simp add: chain_def below_fun_def)
 
 text {* upper bounds of function chains yield upper bound in the po range *}
 
 lemma ub2ub_fun:
   "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
-by (auto simp add: is_ub_def less_fun_def)
+by (auto simp add: is_ub_def below_fun_def)
 
 text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
 
@@ -70,9 +70,9 @@
   shows "range Y <<| f"
 apply (rule is_lubI)
 apply (rule ub_rangeI)
-apply (rule less_fun_ext)
+apply (rule below_fun_ext)
 apply (rule is_ub_lub [OF f])
-apply (rule less_fun_ext)
+apply (rule below_fun_ext)
 apply (rule is_lub_lub [OF f])
 apply (erule ub2ub_fun)
 done
@@ -103,7 +103,7 @@
 proof
   fix f g :: "'a \<Rightarrow> 'b"
   show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
-    unfolding expand_fun_less expand_fun_eq
+    unfolding expand_fun_below expand_fun_eq
     by simp
 qed
 
@@ -148,7 +148,7 @@
 subsection {* Full function space is pointed *}
 
 lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
-by (simp add: less_fun_def)
+by (simp add: below_fun_def)
 
 lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
 apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
@@ -171,13 +171,13 @@
 *}
 
 lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
-by (simp add: less_fun_def)
+by (simp add: below_fun_def)
 
 lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
 by (rule monofunE)
 
 lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
-by (rule trans_less [OF monofun_fun_arg monofun_fun_fun])
+by (rule below_trans [OF monofun_fun_arg monofun_fun_fun])
 
 subsection {* Propagation of monotonicity and continuity *}
 
@@ -236,7 +236,7 @@
 lemma mono2mono_lambda:
   assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
 apply (rule monofunI)
-apply (rule less_fun_ext)
+apply (rule below_fun_ext)
 apply (erule monofunE [OF f])
 done
 
@@ -296,4 +296,3 @@
 by (rule cont2cont_app2 [OF cont_const])
 
 end
-
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Fix.thy	Fri May 08 16:19:51 2009 -0700
@@ -90,7 +90,7 @@
 apply simp
 done
 
-lemma fix_least_less: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
+lemma fix_least_below: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
 apply (simp add: fix_def2)
 apply (rule is_lub_thelub)
 apply (rule chain_iterate)
@@ -98,17 +98,17 @@
 apply (induct_tac i)
 apply simp
 apply simp
-apply (erule rev_trans_less)
+apply (erule rev_below_trans)
 apply (erule monofun_cfun_arg)
 done
 
 lemma fix_least: "F\<cdot>x = x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
-by (rule fix_least_less, simp)
+by (rule fix_least_below, simp)
 
 lemma fix_eqI:
   assumes fixed: "F\<cdot>x = x" and least: "\<And>z. F\<cdot>z = z \<Longrightarrow> x \<sqsubseteq> z"
   shows "fix\<cdot>F = x"
-apply (rule antisym_less)
+apply (rule below_antisym)
 apply (rule fix_least [OF fixed])
 apply (rule least [OF fix_eq [symmetric]])
 done
@@ -230,10 +230,10 @@
   have "?y1 \<sqsubseteq> y" by (rule fix_least, simp add: F_y)
   hence "cfst\<cdot>(F\<cdot>\<langle>x, ?y1\<rangle>) \<sqsubseteq> cfst\<cdot>(F\<cdot>\<langle>x, y\<rangle>)" by (simp add: monofun_cfun)
   hence "cfst\<cdot>(F\<cdot>\<langle>x, ?y1\<rangle>) \<sqsubseteq> x" using F_x by simp
-  hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_less)
+  hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_below)
   hence "csnd\<cdot>(F\<cdot>\<langle>?x, y\<rangle>) \<sqsubseteq> csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>)" by (simp add: monofun_cfun)
   hence "csnd\<cdot>(F\<cdot>\<langle>?x, y\<rangle>) \<sqsubseteq> y" using F_y by simp
-  hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_less)
+  hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_below)
   show "\<langle>?x, ?y\<rangle> \<sqsubseteq> z" using z 1 2 by simp
 qed
 
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/HOLCF.thy	Fri May 08 16:19:51 2009 -0700
@@ -21,4 +21,58 @@
         (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
 *}
 
+text {* Legacy theorem names *}
+
+lemmas sq_ord_less_eq_trans = below_eq_trans
+lemmas sq_ord_eq_less_trans = eq_below_trans
+lemmas refl_less = below_refl
+lemmas trans_less = below_trans
+lemmas antisym_less = below_antisym
+lemmas antisym_less_inverse = below_antisym_inverse
+lemmas box_less = box_below
+lemmas rev_trans_less = rev_below_trans
+lemmas not_less2not_eq = not_below2not_eq
+lemmas less_UU_iff = below_UU_iff
+lemmas flat_less_iff = flat_below_iff
+lemmas adm_less = adm_below
+lemmas adm_not_less = adm_not_below
+lemmas adm_compact_not_less = adm_compact_not_below
+lemmas less_fun_def = below_fun_def
+lemmas expand_fun_less = expand_fun_below
+lemmas less_fun_ext = below_fun_ext
+lemmas less_discr_def = below_discr_def
+lemmas discr_less_eq = discr_below_eq
+lemmas less_unit_def = below_unit_def
+lemmas less_cprod_def = below_prod_def
+lemmas prod_lessI = prod_belowI
+lemmas Pair_less_iff = Pair_below_iff
+lemmas fst_less_iff = fst_below_iff
+lemmas snd_less_iff = snd_below_iff
+lemmas expand_cfun_less = expand_cfun_below
+lemmas less_cfun_ext = below_cfun_ext
+lemmas injection_less = injection_below
+lemmas approx_less = approx_below
+lemmas profinite_less_ext = profinite_below_ext
+lemmas less_up_def = below_up_def
+lemmas not_Iup_less = not_Iup_below
+lemmas Iup_less = Iup_below
+lemmas up_less = up_below
+lemmas cpair_less = cpair_below
+lemmas less_cprod = below_cprod
+lemmas cfst_less_iff = cfst_below_iff
+lemmas csnd_less_iff = csnd_below_iff
+lemmas Def_inject_less_eq = Def_below_Def
+lemmas Def_less_is_eq = Def_below_iff
+lemmas spair_less_iff = spair_below_iff
+lemmas less_sprod = below_sprod
+lemmas spair_less = spair_below
+lemmas sfst_less_iff = sfst_below_iff
+lemmas ssnd_less_iff = ssnd_below_iff
+lemmas fix_least_less = fix_least_below
+lemmas dist_less_one = dist_below_one
+lemmas less_ONE = below_ONE
+lemmas ONE_less_iff = ONE_below_iff
+lemmas less_sinlD = below_sinlD
+lemmas less_sinrD = below_sinrD
+
 end
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Lift.thy
--- 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
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/LowerPD.thy	Fri May 08 16:19:51 2009 -0700
@@ -23,7 +23,7 @@
 apply (drule (1) bspec, erule bexE)
 apply (drule (1) bspec, erule bexE)
 apply (erule rev_bexI)
-apply (erule (1) trans_less)
+apply (erule (1) below_trans)
 done
 
 interpretation lower_le: preorder lower_le
@@ -39,7 +39,7 @@
 lemma PDPlus_lower_mono: "\<lbrakk>s \<le>\<flat> t; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<flat> PDPlus t v"
 unfolding lower_le_def Rep_PDPlus by fast
 
-lemma PDPlus_lower_less: "t \<le>\<flat> PDPlus t u"
+lemma PDPlus_lower_le: "t \<le>\<flat> PDPlus t u"
 unfolding lower_le_def Rep_PDPlus by fast
 
 lemma lower_le_PDUnit_PDUnit_iff [simp]:
@@ -99,7 +99,7 @@
   "{S::'a pd_basis set. lower_le.ideal S}"
 by (fast intro: lower_le.ideal_principal)
 
-instantiation lower_pd :: (profinite) sq_ord
+instantiation lower_pd :: (profinite) below
 begin
 
 definition
@@ -110,16 +110,16 @@
 
 instance lower_pd :: (profinite) po
 by (rule lower_le.typedef_ideal_po
-    [OF type_definition_lower_pd sq_le_lower_pd_def])
+    [OF type_definition_lower_pd below_lower_pd_def])
 
 instance lower_pd :: (profinite) cpo
 by (rule lower_le.typedef_ideal_cpo
-    [OF type_definition_lower_pd sq_le_lower_pd_def])
+    [OF type_definition_lower_pd below_lower_pd_def])
 
 lemma Rep_lower_pd_lub:
   "chain Y \<Longrightarrow> Rep_lower_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_lower_pd (Y i))"
 by (rule lower_le.typedef_ideal_rep_contlub
-    [OF type_definition_lower_pd sq_le_lower_pd_def])
+    [OF type_definition_lower_pd below_lower_pd_def])
 
 lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd xs)"
 by (rule Rep_lower_pd [unfolded mem_Collect_eq])
@@ -145,7 +145,7 @@
 apply (rule ideal_Rep_lower_pd)
 apply (erule Rep_lower_pd_lub)
 apply (rule Rep_lower_principal)
-apply (simp only: sq_le_lower_pd_def)
+apply (simp only: below_lower_pd_def)
 done
 
 text {* Lower powerdomain is pointed *}
@@ -264,28 +264,28 @@
 lemmas lower_plus_aci =
   lower_plus_ac lower_plus_absorb lower_plus_left_absorb
 
-lemma lower_plus_less1: "xs \<sqsubseteq> xs +\<flat> ys"
+lemma lower_plus_below1: "xs \<sqsubseteq> xs +\<flat> ys"
 apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
-apply (simp add: PDPlus_lower_less)
+apply (simp add: PDPlus_lower_le)
 done
 
-lemma lower_plus_less2: "ys \<sqsubseteq> xs +\<flat> ys"
-by (subst lower_plus_commute, rule lower_plus_less1)
+lemma lower_plus_below2: "ys \<sqsubseteq> xs +\<flat> ys"
+by (subst lower_plus_commute, rule lower_plus_below1)
 
 lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs +\<flat> ys \<sqsubseteq> zs"
 apply (subst lower_plus_absorb [of zs, symmetric])
 apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
 done
 
-lemma lower_plus_less_iff:
+lemma lower_plus_below_iff:
   "xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
 apply safe
-apply (erule trans_less [OF lower_plus_less1])
-apply (erule trans_less [OF lower_plus_less2])
+apply (erule below_trans [OF lower_plus_below1])
+apply (erule below_trans [OF lower_plus_below2])
 apply (erule (1) lower_plus_least)
 done
 
-lemma lower_unit_less_plus_iff:
+lemma lower_unit_below_plus_iff:
   "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
  apply (rule iffI)
   apply (subgoal_tac
@@ -299,13 +299,13 @@
    apply simp
   apply simp
  apply (erule disjE)
-  apply (erule trans_less [OF _ lower_plus_less1])
- apply (erule trans_less [OF _ lower_plus_less2])
+  apply (erule below_trans [OF _ lower_plus_below1])
+ apply (erule below_trans [OF _ lower_plus_below2])
 done
 
-lemma lower_unit_less_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
+lemma lower_unit_below_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
  apply (rule iffI)
-  apply (rule profinite_less_ext)
+  apply (rule profinite_below_ext)
   apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
@@ -313,10 +313,10 @@
  apply (erule monofun_cfun_arg)
 done
 
-lemmas lower_pd_less_simps =
-  lower_unit_less_iff
-  lower_plus_less_iff
-  lower_unit_less_plus_iff
+lemmas lower_pd_below_simps =
+  lower_unit_below_iff
+  lower_plus_below_iff
+  lower_unit_below_plus_iff
 
 lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y"
 by (simp add: po_eq_conv)
@@ -330,18 +330,18 @@
 lemma lower_plus_strict_iff [simp]:
   "xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
 apply safe
-apply (rule UU_I, erule subst, rule lower_plus_less1)
-apply (rule UU_I, erule subst, rule lower_plus_less2)
+apply (rule UU_I, erule subst, rule lower_plus_below1)
+apply (rule UU_I, erule subst, rule lower_plus_below2)
 apply (rule lower_plus_absorb)
 done
 
 lemma lower_plus_strict1 [simp]: "\<bottom> +\<flat> ys = ys"
-apply (rule antisym_less [OF _ lower_plus_less2])
+apply (rule below_antisym [OF _ lower_plus_below2])
 apply (simp add: lower_plus_least)
 done
 
 lemma lower_plus_strict2 [simp]: "xs +\<flat> \<bottom> = xs"
-apply (rule antisym_less [OF _ lower_plus_less1])
+apply (rule below_antisym [OF _ lower_plus_below1])
 apply (simp add: lower_plus_least)
 done
 
@@ -412,11 +412,11 @@
 
 lemma lower_bind_basis_mono:
   "t \<le>\<flat> u \<Longrightarrow> lower_bind_basis t \<sqsubseteq> lower_bind_basis u"
-unfolding expand_cfun_less
+unfolding expand_cfun_below
 apply (erule lower_le_induct, safe)
 apply (simp add: monofun_cfun)
-apply (simp add: rev_trans_less [OF lower_plus_less1])
-apply (simp add: lower_plus_less_iff)
+apply (simp add: rev_below_trans [OF lower_plus_below1])
+apply (simp add: lower_plus_below_iff)
 done
 
 definition
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/One.thy	Fri May 08 16:19:51 2009 -0700
@@ -28,13 +28,13 @@
 lemma one_induct: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
 by (cases x rule: oneE) simp_all
 
-lemma dist_less_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
+lemma dist_below_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
 unfolding ONE_def by simp
 
-lemma less_ONE [simp]: "x \<sqsubseteq> ONE"
+lemma below_ONE [simp]: "x \<sqsubseteq> ONE"
 by (induct x rule: one_induct) simp_all
 
-lemma ONE_less_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
+lemma ONE_below_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
 by (induct x rule: one_induct) simp_all
 
 lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>"
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Pcpo.thy	Fri May 08 16:19:51 2009 -0700
@@ -46,7 +46,7 @@
 
 lemma lub_range_shift:
   "chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)"
-apply (rule antisym_less)
+apply (rule below_antisym)
 apply (rule lub_range_mono)
 apply    fast
 apply   assumption
@@ -54,7 +54,7 @@
 apply (rule is_lub_thelub)
 apply assumption
 apply (rule ub_rangeI)
-apply (rule_tac y="Y (i + j)" in trans_less)
+apply (rule_tac y="Y (i + j)" in below_trans)
 apply (erule chain_mono)
 apply (rule le_add1)
 apply (rule is_ub_thelub)
@@ -66,7 +66,7 @@
 apply (rule iffI)
 apply (fast intro!: thelubI lub_finch1)
 apply (unfold max_in_chain_def)
-apply (safe intro!: antisym_less)
+apply (safe intro!: below_antisym)
 apply (fast elim!: chain_mono)
 apply (drule sym)
 apply (force elim!: is_ub_thelub)
@@ -79,7 +79,7 @@
     \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
 apply (erule is_lub_thelub)
 apply (rule ub_rangeI)
-apply (rule trans_less)
+apply (rule below_trans)
 apply (erule meta_spec)
 apply (erule is_ub_thelub)
 done
@@ -106,7 +106,7 @@
 lemma lub_equal2:
   "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
     \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
-  by (blast intro: antisym_less lub_mono2 sym)
+  by (blast intro: below_antisym lub_mono2 sym)
 
 lemma lub_mono3:
   "\<lbrakk>chain Y; chain X; \<forall>i. \<exists>j. Y i \<sqsubseteq> X j\<rbrakk>
@@ -115,7 +115,7 @@
 apply (rule ub_rangeI)
 apply (erule allE)
 apply (erule exE)
-apply (erule trans_less)
+apply (erule below_trans)
 apply (erule is_ub_thelub)
 done
 
@@ -132,10 +132,10 @@
   assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
   assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
   shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)"
-proof (rule antisym_less)
+proof (rule below_antisym)
   have 3: "chain (\<lambda>i. Y i i)"
     apply (rule chainI)
-    apply (rule trans_less)
+    apply (rule below_trans)
     apply (rule chainE [OF 1])
     apply (rule chainE [OF 2])
     done
@@ -146,7 +146,7 @@
     apply (rule ub_rangeI)
     apply (rule lub_mono3 [rule_format, OF 2 3])
     apply (rule exI)
-    apply (rule trans_less)
+    apply (rule below_trans)
     apply (rule chain_mono [OF 1 le_maxI1])
     apply (rule chain_mono [OF 2 le_maxI2])
     done
@@ -185,7 +185,7 @@
 apply (rule theI')
 apply (rule ex_ex1I)
 apply (rule least)
-apply (blast intro: antisym_less)
+apply (blast intro: below_antisym)
 done
 
 lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
@@ -207,7 +207,7 @@
 
 text {* useful lemmas about @{term \<bottom>} *}
 
-lemma less_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
+lemma below_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
 by (simp add: po_eq_conv)
 
 lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
@@ -287,7 +287,7 @@
 apply (blast dest: chain_mono ax_flat)
 done
 
-lemma flat_less_iff:
+lemma flat_below_iff:
   shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
   by (safe dest!: ax_flat)
 
@@ -298,7 +298,7 @@
 
 text {* Discrete cpos *}
 
-class discrete_cpo = sq_ord +
+class discrete_cpo = below +
   assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
 begin
 
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Pcpodef.thy	Fri May 08 16:19:51 2009 -0700
@@ -16,22 +16,22 @@
   if the ordering is defined in the standard way.
 *}
 
-setup {* Sign.add_const_constraint (@{const_name Porder.sq_le}, NONE) *}
+setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
 
 theorem typedef_po:
   fixes Abs :: "'a::po \<Rightarrow> 'b::type"
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   shows "OFCLASS('b, po_class)"
- apply (intro_classes, unfold less)
-   apply (rule refl_less)
-  apply (erule (1) trans_less)
+ apply (intro_classes, unfold below)
+   apply (rule below_refl)
+  apply (erule (1) below_trans)
  apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
- apply (erule (1) antisym_less)
+ apply (erule (1) below_antisym)
 done
 
-setup {* Sign.add_const_constraint (@{const_name Porder.sq_le},
-  SOME @{typ "'a::sq_ord \<Rightarrow> 'a::sq_ord \<Rightarrow> bool"}) *}
+setup {* Sign.add_const_constraint (@{const_name Porder.below},
+  SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
 
 subsection {* Proving a subtype is finite *}
 
@@ -58,9 +58,9 @@
 subsection {* Proving a subtype is chain-finite *}
 
 lemma monofun_Rep:
-  assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   shows "monofun Rep"
-by (rule monofunI, unfold less)
+by (rule monofunI, unfold below)
 
 lemmas ch2ch_Rep = ch2ch_monofun [OF monofun_Rep]
 lemmas ub2ub_Rep = ub2ub_monofun [OF monofun_Rep]
@@ -68,10 +68,10 @@
 theorem typedef_chfin:
   fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   shows "OFCLASS('b, chfin_class)"
  apply intro_classes
- apply (drule ch2ch_Rep [OF less])
+ apply (drule ch2ch_Rep [OF below])
  apply (drule chfin)
  apply (unfold max_in_chain_def)
  apply (simp add: type_definition.Rep_inject [OF type])
@@ -90,28 +90,28 @@
 lemma Abs_inverse_lub_Rep:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and adm:  "adm (\<lambda>x. x \<in> A)"
   shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
  apply (rule type_definition.Abs_inverse [OF type])
- apply (erule admD [OF adm ch2ch_Rep [OF less]])
+ apply (erule admD [OF adm ch2ch_Rep [OF below]])
  apply (rule type_definition.Rep [OF type])
 done
 
 theorem typedef_lub:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and adm: "adm (\<lambda>x. x \<in> A)"
   shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
- apply (frule ch2ch_Rep [OF less])
+ apply (frule ch2ch_Rep [OF below])
  apply (rule is_lubI)
   apply (rule ub_rangeI)
-  apply (simp only: less Abs_inverse_lub_Rep [OF type less adm])
+  apply (simp only: below Abs_inverse_lub_Rep [OF type below adm])
   apply (erule is_ub_thelub)
- apply (simp only: less Abs_inverse_lub_Rep [OF type less adm])
+ apply (simp only: below Abs_inverse_lub_Rep [OF type below adm])
  apply (erule is_lub_thelub)
- apply (erule ub2ub_Rep [OF less])
+ apply (erule ub2ub_Rep [OF below])
 done
 
 lemmas typedef_thelub = typedef_lub [THEN thelubI, standard]
@@ -119,13 +119,13 @@
 theorem typedef_cpo:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and adm: "adm (\<lambda>x. x \<in> A)"
   shows "OFCLASS('b, cpo_class)"
 proof
   fix S::"nat \<Rightarrow> 'b" assume "chain S"
   hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
-    by (rule typedef_lub [OF type less adm])
+    by (rule typedef_lub [OF type below adm])
   thus "\<exists>x. range S <<| x" ..
 qed
 
@@ -136,14 +136,14 @@
 theorem typedef_cont_Rep:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and adm: "adm (\<lambda>x. x \<in> A)"
   shows "cont Rep"
  apply (rule contI)
- apply (simp only: typedef_thelub [OF type less adm])
- apply (simp only: Abs_inverse_lub_Rep [OF type less adm])
+ apply (simp only: typedef_thelub [OF type below adm])
+ apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
  apply (rule cpo_lubI)
- apply (erule ch2ch_Rep [OF less])
+ apply (erule ch2ch_Rep [OF below])
 done
 
 text {*
@@ -153,28 +153,28 @@
 *}
 
 theorem typedef_is_lubI:
-  assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
  apply (rule is_lubI)
   apply (rule ub_rangeI)
-  apply (subst less)
+  apply (subst below)
   apply (erule is_ub_lub)
- apply (subst less)
+ apply (subst below)
  apply (erule is_lub_lub)
- apply (erule ub2ub_Rep [OF less])
+ apply (erule ub2ub_Rep [OF below])
 done
 
 theorem typedef_cont_Abs:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
     and f_in_A: "\<And>x. f x \<in> A"
     and cont_f: "cont f"
   shows "cont (\<lambda>x. Abs (f x))"
  apply (rule contI)
- apply (rule typedef_is_lubI [OF less])
+ apply (rule typedef_is_lubI [OF below])
  apply (simp only: type_definition.Abs_inverse [OF type f_in_A])
  apply (erule cont_f [THEN contE])
 done
@@ -184,15 +184,15 @@
 theorem typedef_compact:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and adm: "adm (\<lambda>x. x \<in> A)"
   shows "compact (Rep k) \<Longrightarrow> compact k"
 proof (unfold compact_def)
   have cont_Rep: "cont Rep"
-    by (rule typedef_cont_Rep [OF type less adm])
+    by (rule typedef_cont_Rep [OF type below adm])
   assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
   with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
-  thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold less)
+  thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
 qed
 
 subsection {* Proving a subtype is pointed *}
@@ -205,13 +205,13 @@
 theorem typedef_pcpo_generic:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and z_in_A: "z \<in> A"
     and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
   shows "OFCLASS('b, pcpo_class)"
  apply (intro_classes)
  apply (rule_tac x="Abs z" in exI, rule allI)
- apply (unfold less)
+ apply (unfold below)
  apply (subst type_definition.Abs_inverse [OF type z_in_A])
  apply (rule z_least [OF type_definition.Rep [OF type]])
 done
@@ -224,10 +224,10 @@
 theorem typedef_pcpo:
   fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
   shows "OFCLASS('b, pcpo_class)"
-by (rule typedef_pcpo_generic [OF type less UU_in_A], rule minimal)
+by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
 
 subsubsection {* Strictness of @{term Rep} and @{term Abs} *}
 
@@ -238,66 +238,66 @@
 
 theorem typedef_Abs_strict:
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
   shows "Abs \<bottom> = \<bottom>"
- apply (rule UU_I, unfold less)
+ apply (rule UU_I, unfold below)
  apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
 done
 
 theorem typedef_Rep_strict:
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
   shows "Rep \<bottom> = \<bottom>"
- apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
+ apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
  apply (rule type_definition.Abs_inverse [OF type UU_in_A])
 done
 
 theorem typedef_Abs_strict_iff:
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
   shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
+ apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
  apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
 done
 
 theorem typedef_Rep_strict_iff:
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
   shows "(Rep x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Rep_strict [OF type less UU_in_A, THEN subst])
+ apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
  apply (simp add: type_definition.Rep_inject [OF type])
 done
 
 theorem typedef_Abs_defined:
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
   shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
-by (simp add: typedef_Abs_strict_iff [OF type less UU_in_A])
+by (simp add: typedef_Abs_strict_iff [OF type below UU_in_A])
 
 theorem typedef_Rep_defined:
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
   shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
-by (simp add: typedef_Rep_strict_iff [OF type less UU_in_A])
+by (simp add: typedef_Rep_strict_iff [OF type below UU_in_A])
 
 subsection {* Proving a subtype is flat *}
 
 theorem typedef_flat:
   fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
   assumes type: "type_definition Rep Abs A"
-    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
   shows "OFCLASS('b, flat_class)"
  apply (intro_classes)
- apply (unfold less)
+ apply (unfold below)
  apply (simp add: type_definition.Rep_inject [OF type, symmetric])
- apply (simp add: typedef_Rep_strict [OF type less UU_in_A])
+ apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
  apply (simp add: ax_flat)
 done
 
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Porder.thy	Fri May 08 16:19:51 2009 -0700
@@ -10,59 +10,59 @@
 
 subsection {* Type class for partial orders *}
 
-class sq_ord =
-  fixes sq_le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+class below =
+  fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 begin
 
 notation
-  sq_le (infixl "<<" 55)
+  below (infixl "<<" 55)
 
 notation (xsymbols)
-  sq_le (infixl "\<sqsubseteq>" 55)
+  below (infixl "\<sqsubseteq>" 55)
 
-lemma sq_ord_less_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
+lemma below_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
   by (rule subst)
 
-lemma sq_ord_eq_less_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
+lemma eq_below_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
   by (rule ssubst)
 
 end
 
-class po = sq_ord +
-  assumes refl_less [iff]: "x \<sqsubseteq> x"
-  assumes trans_less: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
-  assumes antisym_less: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
+class po = below +
+  assumes below_refl [iff]: "x \<sqsubseteq> x"
+  assumes below_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
+  assumes below_antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
 begin
 
 text {* minimal fixes least element *}
 
 lemma minimal2UU[OF allI] : "\<forall>x. uu \<sqsubseteq> x \<Longrightarrow> uu = (THE u. \<forall>y. u \<sqsubseteq> y)"
-  by (blast intro: theI2 antisym_less)
+  by (blast intro: theI2 below_antisym)
 
 text {* the reverse law of anti-symmetry of @{term "op <<"} *}
-
-lemma antisym_less_inverse: "x = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
+(* Is this rule ever useful? *)
+lemma below_antisym_inverse: "x = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
   by simp
 
-lemma box_less: "a \<sqsubseteq> b \<Longrightarrow> c \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> c \<sqsubseteq> d"
-  by (rule trans_less [OF trans_less])
+lemma box_below: "a \<sqsubseteq> b \<Longrightarrow> c \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> c \<sqsubseteq> d"
+  by (rule below_trans [OF below_trans])
 
 lemma po_eq_conv: "x = y \<longleftrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
-  by (fast elim!: antisym_less_inverse intro!: antisym_less)
+  by (fast intro!: below_antisym)
 
-lemma rev_trans_less: "y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z"
-  by (rule trans_less)
+lemma rev_below_trans: "y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z"
+  by (rule below_trans)
 
-lemma not_less2not_eq: "\<not> x \<sqsubseteq> y \<Longrightarrow> x \<noteq> y"
+lemma not_below2not_eq: "\<not> x \<sqsubseteq> y \<Longrightarrow> x \<noteq> y"
   by auto
 
 end
 
 lemmas HOLCF_trans_rules [trans] =
-  trans_less
-  antisym_less
-  sq_ord_less_eq_trans
-  sq_ord_eq_less_trans
+  below_trans
+  below_antisym
+  below_eq_trans
+  eq_below_trans
 
 context po
 begin
@@ -97,7 +97,7 @@
   unfolding is_ub_def by fast
 
 lemma is_ub_upward: "\<lbrakk>S <| x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S <| y"
-  unfolding is_ub_def by (fast intro: trans_less)
+  unfolding is_ub_def by (fast intro: below_trans)
 
 subsection {* Least upper bounds *}
 
@@ -143,7 +143,7 @@
 
 lemma unique_lub: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
 apply (unfold is_lub_def is_ub_def)
-apply (blast intro: antisym_less)
+apply (blast intro: below_antisym)
 done
 
 text {* technical lemmas about @{term lub} and @{term is_lub} *}
@@ -191,7 +191,7 @@
 text {* chains are monotone functions *}
 
 lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
-  by (erule less_Suc_induct, erule chainE, erule trans_less)
+  by (erule less_Suc_induct, erule chainE, erule below_trans)
 
 lemma chain_mono: "\<lbrakk>chain Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
   by (cases "i = j", simp, simp add: chain_mono_less)
@@ -208,7 +208,7 @@
   "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x"
 apply (rule iffI)
 apply (rule ub_rangeI)
-apply (rule_tac y="S (i + j)" in trans_less)
+apply (rule_tac y="S (i + j)" in below_trans)
 apply (erule chain_mono)
 apply (rule le_add1)
 apply (erule ub_rangeD)
@@ -313,7 +313,7 @@
   apply (erule exE)
   apply (rule finite_chainI, assumption)
   apply (rule max_in_chainI)
-  apply (rule antisym_less)
+  apply (rule below_antisym)
    apply (erule (1) chain_mono)
   apply (erule spec)
  apply (rule finite_range_has_max)
@@ -451,4 +451,4 @@
 
 end
 
-end
\ No newline at end of file
+end
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Product_Cpo.thy
--- a/src/HOLCF/Product_Cpo.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Product_Cpo.thy	Fri May 08 16:19:51 2009 -0700
@@ -12,11 +12,11 @@
 
 subsection {* Type @{typ unit} is a pcpo *}
 
-instantiation unit :: sq_ord
+instantiation unit :: below
 begin
 
 definition
-  less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
+  below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True"
 
 instance ..
 end
@@ -32,11 +32,11 @@
 
 subsection {* Product type is a partial order *}
 
-instantiation "*" :: (sq_ord, sq_ord) sq_ord
+instantiation "*" :: (below, below) below
 begin
 
 definition
-  less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
+  below_prod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
 
 instance ..
 end
@@ -45,26 +45,26 @@
 proof
   fix x :: "'a \<times> 'b"
   show "x \<sqsubseteq> x"
-    unfolding less_cprod_def by simp
+    unfolding below_prod_def by simp
 next
   fix x y :: "'a \<times> 'b"
   assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
-    unfolding less_cprod_def Pair_fst_snd_eq
-    by (fast intro: antisym_less)
+    unfolding below_prod_def Pair_fst_snd_eq
+    by (fast intro: below_antisym)
 next
   fix x y z :: "'a \<times> 'b"
   assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
-    unfolding less_cprod_def
-    by (fast intro: trans_less)
+    unfolding below_prod_def
+    by (fast intro: below_trans)
 qed
 
 subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
 
-lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
-unfolding less_cprod_def by simp
+lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
+unfolding below_prod_def by simp
 
-lemma Pair_less_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
-unfolding less_cprod_def by simp
+lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
+unfolding below_prod_def by simp
 
 text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
 
@@ -81,20 +81,20 @@
 text {* @{term fst} and @{term snd} are monotone *}
 
 lemma monofun_fst: "monofun fst"
-by (simp add: monofun_def less_cprod_def)
+by (simp add: monofun_def below_prod_def)
 
 lemma monofun_snd: "monofun snd"
-by (simp add: monofun_def less_cprod_def)
+by (simp add: monofun_def below_prod_def)
 
 subsection {* Product type is a cpo *}
 
 lemma is_lub_Pair:
   "\<lbrakk>range X <<| x; range Y <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) <<| (x, y)"
 apply (rule is_lubI [OF ub_rangeI])
-apply (simp add: less_cprod_def is_ub_lub)
+apply (simp add: below_prod_def is_ub_lub)
 apply (frule ub2ub_monofun [OF monofun_fst])
 apply (drule ub2ub_monofun [OF monofun_snd])
-apply (simp add: less_cprod_def is_lub_lub)
+apply (simp add: below_prod_def is_lub_lub)
 done
 
 lemma lub_cprod:
@@ -134,14 +134,14 @@
 proof
   fix x y :: "'a \<times> 'b"
   show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
-    unfolding less_cprod_def Pair_fst_snd_eq
+    unfolding below_prod_def Pair_fst_snd_eq
     by simp
 qed
 
 subsection {* Product type is pointed *}
 
 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
-by (simp add: less_cprod_def)
+by (simp add: below_prod_def)
 
 instance "*" :: (pcpo, pcpo) pcpo
 by intro_classes (fast intro: minimal_cprod)
@@ -257,20 +257,20 @@
 
 subsection {* Compactness and chain-finiteness *}
 
-lemma fst_less_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
-unfolding less_cprod_def by simp
+lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
+unfolding below_prod_def by simp
 
-lemma snd_less_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y = x \<sqsubseteq> (fst x, y)"
-unfolding less_cprod_def by simp
+lemma snd_below_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"
+unfolding below_prod_def by simp
 
 lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
-by (rule compactI, simp add: fst_less_iff)
+by (rule compactI, simp add: fst_below_iff)
 
 lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)"
-by (rule compactI, simp add: snd_less_iff)
+by (rule compactI, simp add: snd_below_iff)
 
 lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)"
-by (rule compactI, simp add: less_cprod_def)
+by (rule compactI, simp add: below_prod_def)
 
 lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y"
 apply (safe intro!: compact_Pair)
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Sprod.thy	Fri May 08 16:19:51 2009 -0700
@@ -20,7 +20,7 @@
 by (rule typedef_finite_po [OF type_definition_Sprod])
 
 instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
-by (rule typedef_chfin [OF type_definition_Sprod less_Sprod_def])
+by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
 
 syntax (xsymbols)
   "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
@@ -67,7 +67,7 @@
 by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
 
 lemmas Rep_Sprod_simps =
-  Rep_Sprod_inject [symmetric] less_Sprod_def
+  Rep_Sprod_inject [symmetric] below_Sprod_def
   Rep_Sprod_strict Rep_Sprod_spair
 
 lemma Exh_Sprod:
@@ -99,7 +99,7 @@
 lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
 by (simp add: Rep_Sprod_simps strictify_conv_if)
 
-lemma spair_less_iff:
+lemma spair_below_iff:
   "((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))"
 by (simp add: Rep_Sprod_simps strictify_conv_if)
 
@@ -160,38 +160,38 @@
 lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
 by (cases p, simp_all)
 
-lemma less_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
-apply (simp add: less_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
-apply (rule less_cprod)
+lemma below_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
+apply (simp add: below_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
+apply (rule below_cprod)
 done
 
 lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)"
-by (auto simp add: po_eq_conv less_sprod)
+by (auto simp add: po_eq_conv below_sprod)
 
-lemma spair_less:
+lemma spair_below:
   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)"
 apply (cases "a = \<bottom>", simp)
 apply (cases "b = \<bottom>", simp)
-apply (simp add: less_sprod)
+apply (simp add: below_sprod)
 done
 
-lemma sfst_less_iff: "sfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
+lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
 apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
-apply (simp add: less_sprod)
+apply (simp add: below_sprod)
 done
 
-lemma ssnd_less_iff: "ssnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:sfst\<cdot>x, y:)"
+lemma ssnd_below_iff: "ssnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:sfst\<cdot>x, y:)"
 apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
-apply (simp add: less_sprod)
+apply (simp add: below_sprod)
 done
 
 subsection {* Compactness *}
 
 lemma compact_sfst: "compact x \<Longrightarrow> compact (sfst\<cdot>x)"
-by (rule compactI, simp add: sfst_less_iff)
+by (rule compactI, simp add: sfst_below_iff)
 
 lemma compact_ssnd: "compact x \<Longrightarrow> compact (ssnd\<cdot>x)"
-by (rule compactI, simp add: ssnd_less_iff)
+by (rule compactI, simp add: ssnd_below_iff)
 
 lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
 by (rule compact_Sprod, simp add: Rep_Sprod_spair strictify_conv_if)
@@ -224,7 +224,7 @@
   assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
     apply (induct x, simp)
     apply (induct y, simp)
-    apply (simp add: spair_less_iff flat_less_iff)
+    apply (simp add: spair_below_iff flat_below_iff)
     done
 qed
 
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Ssum.thy	Fri May 08 16:19:51 2009 -0700
@@ -22,7 +22,7 @@
 by (rule typedef_finite_po [OF type_definition_Ssum])
 
 instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
-by (rule typedef_chfin [OF type_definition_Ssum less_Ssum_def])
+by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
 
 syntax (xsymbols)
   "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
@@ -61,17 +61,17 @@
 
 text {* Ordering *}
 
-lemma sinl_less [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl strictify_conv_if)
+lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
+by (simp add: below_Ssum_def Rep_Ssum_sinl strictify_conv_if)
 
-lemma sinr_less [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: less_Ssum_def Rep_Ssum_sinr strictify_conv_if)
+lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
+by (simp add: below_Ssum_def Rep_Ssum_sinr strictify_conv_if)
 
-lemma sinl_less_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
+lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
+by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
 
-lemma sinr_less_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
+lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
+by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
 
 text {* Equality *}
 
@@ -167,10 +167,10 @@
   "\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
 by (cases p, simp only: sinl_strict [symmetric], simp, simp)
 
-lemma less_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"
+lemma below_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"
 by (cases p, rule_tac x="\<bottom>" in exI, simp_all)
 
-lemma less_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
+lemma below_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
 by (cases p, rule_tac x="\<bottom>" in exI, simp_all)
 
 subsection {* Case analysis combinator *}
@@ -207,8 +207,8 @@
 instance "++" :: (flat, flat) flat
 apply (intro_classes, clarify)
 apply (rule_tac p=x in ssumE, simp)
-apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
-apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
+apply (rule_tac p=y in ssumE, simp_all add: flat_below_iff)
+apply (rule_tac p=y in ssumE, simp_all add: flat_below_iff)
 done
 
 subsection {* Strict sum is a bifinite domain *}
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Sum_Cpo.thy
--- a/src/HOLCF/Sum_Cpo.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Sum_Cpo.thy	Fri May 08 16:19:51 2009 -0700
@@ -10,28 +10,28 @@
 
 subsection {* Ordering on type @{typ "'a + 'b"} *}
 
-instantiation "+" :: (sq_ord, sq_ord) sq_ord
+instantiation "+" :: (below, below) below
 begin
 
-definition
-  less_sum_def: "x \<sqsubseteq> y \<equiv> case x of
+definition below_sum_def:
+  "x \<sqsubseteq> y \<equiv> case x of
          Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) |
          Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)"
 
 instance ..
 end
 
-lemma Inl_less_iff [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
-unfolding less_sum_def by simp
+lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
+unfolding below_sum_def by simp
 
-lemma Inr_less_iff [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
-unfolding less_sum_def by simp
+lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
+unfolding below_sum_def by simp
 
-lemma Inl_less_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
-unfolding less_sum_def by simp
+lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
+unfolding below_sum_def by simp
 
-lemma Inr_less_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
-unfolding less_sum_def by simp
+lemma Inr_below_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
+unfolding below_sum_def by simp
 
 lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
 by simp
@@ -39,20 +39,20 @@
 lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
 by simp
 
-lemma Inl_lessE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+lemma Inl_belowE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
 by (cases x, simp_all)
 
-lemma Inr_lessE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+lemma Inr_belowE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
 by (cases x, simp_all)
 
-lemmas sum_less_elims = Inl_lessE Inr_lessE
+lemmas sum_below_elims = Inl_belowE Inr_belowE
 
-lemma sum_less_cases:
+lemma sum_below_cases:
   "\<lbrakk>x \<sqsubseteq> y;
     \<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R;
     \<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk>
       \<Longrightarrow> R"
-by (cases x, safe elim!: sum_less_elims, auto)
+by (cases x, safe elim!: sum_below_elims, auto)
 
 subsection {* Sum type is a complete partial order *}
 
@@ -64,18 +64,18 @@
 next
   fix x y :: "'a + 'b"
   assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
-    by (induct x, auto elim!: sum_less_elims intro: antisym_less)
+    by (induct x, auto elim!: sum_below_elims intro: below_antisym)
 next
   fix x y z :: "'a + 'b"
   assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
-    by (induct x, auto elim!: sum_less_elims intro: trans_less)
+    by (induct x, auto elim!: sum_below_elims intro: below_trans)
 qed
 
 lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
-by (rule monofunI, erule sum_less_cases, simp_all)
+by (rule monofunI, erule sum_below_cases, simp_all)
 
 lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
-by (rule monofunI, erule sum_less_cases, simp_all)
+by (rule monofunI, erule sum_below_cases, simp_all)
 
 lemma sum_chain_cases:
   assumes Y: "chain Y"
@@ -87,12 +87,12 @@
    apply (rule ch2ch_monofun [OF monofun_inv_Inl Y])
   apply (rule ext)
   apply (cut_tac j=i in chain_mono [OF Y le0], simp)
-  apply (erule Inl_lessE, simp)
+  apply (erule Inl_belowE, simp)
  apply (rule B)
   apply (rule ch2ch_monofun [OF monofun_inv_Inr Y])
  apply (rule ext)
  apply (cut_tac j=i in chain_mono [OF Y le0], simp)
- apply (erule Inr_lessE, simp)
+ apply (erule Inr_belowE, simp)
 done
 
 lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
@@ -100,7 +100,7 @@
   apply (rule ub_rangeI)
   apply (simp add: is_ub_lub)
  apply (frule ub_rangeD [where i=arbitrary])
- apply (erule Inl_lessE, simp)
+ apply (erule Inl_belowE, simp)
  apply (erule is_lub_lub)
  apply (rule ub_rangeI)
  apply (drule ub_rangeD, simp)
@@ -111,7 +111,7 @@
   apply (rule ub_rangeI)
   apply (simp add: is_ub_lub)
  apply (frule ub_rangeD [where i=arbitrary])
- apply (erule Inr_lessE, simp)
+ apply (erule Inr_belowE, simp)
  apply (erule is_lub_lub)
  apply (rule ub_rangeI)
  apply (drule ub_rangeD, simp)
@@ -226,7 +226,7 @@
 instance "+" :: (finite_po, finite_po) finite_po ..
 
 instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo
-by intro_classes (simp add: less_sum_def split: sum.split)
+by intro_classes (simp add: below_sum_def split: sum.split)
 
 subsection {* Sum type is a bifinite domain *}
 
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Tools/domain/domain_library.ML
--- a/src/HOLCF/Tools/domain/domain_library.ML	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Fri May 08 16:19:51 2009 -0700
@@ -257,7 +257,7 @@
 infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
 infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
 infix 1 ~=;     fun S ~=  T = HOLogic.mk_not (S === T);
-infix 1 <<;     fun S <<  T = %%: @{const_name Porder.sq_le} $ S $ T;
+infix 1 <<;     fun S <<  T = %%: @{const_name Porder.below} $ S $ T;
 infix 1 ~<<;    fun S ~<< T = HOLogic.mk_not (S << T);
 
 infix 9 `  ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Fri May 08 16:19:51 2009 -0700
@@ -29,7 +29,7 @@
 val adm_all = @{thm adm_all};
 val adm_conj = @{thm adm_conj};
 val adm_subst = @{thm adm_subst};
-val antisym_less_inverse = @{thm antisym_less_inverse};
+val antisym_less_inverse = @{thm below_antisym_inverse};
 val beta_cfun = @{thm beta_cfun};
 val cfun_arg_cong = @{thm cfun_arg_cong};
 val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL};
@@ -44,12 +44,12 @@
 val contlub_cfun_fun = @{thm contlub_cfun_fun};
 val fix_def2 = @{thm fix_def2};
 val injection_eq = @{thm injection_eq};
-val injection_less = @{thm injection_less};
+val injection_less = @{thm injection_below};
 val lub_equal = @{thm lub_equal};
 val monofun_cfun_arg = @{thm monofun_cfun_arg};
 val retraction_strict = @{thm retraction_strict};
 val spair_eq = @{thm spair_eq};
-val spair_less = @{thm spair_less};
+val spair_less = @{thm spair_below};
 val sscase1 = @{thm sscase1};
 val ssplit1 = @{thm ssplit1};
 val strictify1 = @{thm strictify1};
@@ -121,7 +121,7 @@
 
 val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
 
-val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: antisym_less_inverse)}
+val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)}
 
 in
 
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Fri May 08 16:19:51 2009 -0700
@@ -66,9 +66,9 @@
         NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
       | SOME morphs => morphs);
     val RepC = Const (full Rep_name, newT --> oldT);
-    fun lessC T = Const (@{const_name sq_le}, T --> T --> HOLogic.boolT);
-    val less_def = Logic.mk_equals (lessC newT,
-      Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
+    fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
+    val below_def = Logic.mk_equals (belowC newT,
+      Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
 
     fun make_po tac thy1 =
       let
@@ -76,22 +76,22 @@
           |> TypedefPackage.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
         val lthy3 = thy2
           |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
-        val less_def' = Syntax.check_term lthy3 less_def;
-        val ((_, (_, less_definition')), lthy4) = lthy3
+        val below_def' = Syntax.check_term lthy3 below_def;
+        val ((_, (_, below_definition')), lthy4) = lthy3
           |> Specification.definition (NONE,
-              ((Binding.prefix_name "less_" (Binding.suffix_name "_def" name), []), less_def'));
+              ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
         val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
-        val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
+        val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
         val thy5 = lthy4
           |> Class.prove_instantiation_instance
-              (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, less_definition]) 1))
+              (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
           |> LocalTheory.exit_global;
-      in ((type_definition, less_definition, set_def), thy5) end;
+      in ((type_definition, below_definition, set_def), thy5) end;
 
-    fun make_cpo admissible (type_def, less_def, set_def) theory =
+    fun make_cpo admissible (type_def, below_def, set_def) theory =
       let
         val admissible' = fold_rule (the_list set_def) admissible;
-        val cpo_thms = map (Thm.transfer theory) [type_def, less_def, admissible'];
+        val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
         val theory' = theory
           |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
             (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
@@ -110,10 +110,10 @@
         |> Sign.parent_path
       end;
 
-    fun make_pcpo UU_mem (type_def, less_def, set_def) theory =
+    fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
       let
         val UU_mem' = fold_rule (the_list set_def) UU_mem;
-        val pcpo_thms = map (Thm.transfer theory) [type_def, less_def, UU_mem'];
+        val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
         val theory' = theory
           |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
             (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Tr.thy	Fri May 08 16:19:51 2009 -0700
@@ -37,7 +37,7 @@
 
 text {* distinctness for type @{typ tr} *}
 
-lemma dist_less_tr [simp]:
+lemma dist_below_tr [simp]:
   "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
 unfolding TT_def FF_def by simp_all
 
@@ -45,16 +45,16 @@
   "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
 unfolding TT_def FF_def by simp_all
 
-lemma TT_less_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
+lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
 by (induct x rule: tr_induct) simp_all
 
-lemma FF_less_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
+lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
 by (induct x rule: tr_induct) simp_all
 
-lemma not_less_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
+lemma not_below_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
 by (induct x rule: tr_induct) simp_all
 
-lemma not_less_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
+lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
 by (induct x rule: tr_induct) simp_all
 
 
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Universal.thy
--- a/src/HOLCF/Universal.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Universal.thy	Fri May 08 16:19:51 2009 -0700
@@ -251,7 +251,7 @@
 typedef (open) udom = "{S. udom.ideal S}"
 by (fast intro: udom.ideal_principal)
 
-instantiation udom :: sq_ord
+instantiation udom :: below
 begin
 
 definition
@@ -262,16 +262,16 @@
 
 instance udom :: po
 by (rule udom.typedef_ideal_po
-    [OF type_definition_udom sq_le_udom_def])
+    [OF type_definition_udom below_udom_def])
 
 instance udom :: cpo
 by (rule udom.typedef_ideal_cpo
-    [OF type_definition_udom sq_le_udom_def])
+    [OF type_definition_udom below_udom_def])
 
 lemma Rep_udom_lub:
   "chain Y \<Longrightarrow> Rep_udom (\<Squnion>i. Y i) = (\<Union>i. Rep_udom (Y i))"
 by (rule udom.typedef_ideal_rep_contlub
-    [OF type_definition_udom sq_le_udom_def])
+    [OF type_definition_udom below_udom_def])
 
 lemma ideal_Rep_udom: "udom.ideal (Rep_udom xs)"
 by (rule Rep_udom [unfolded mem_Collect_eq])
@@ -291,7 +291,7 @@
 apply (rule ideal_Rep_udom)
 apply (erule Rep_udom_lub)
 apply (rule Rep_udom_principal)
-apply (simp only: sq_le_udom_def)
+apply (simp only: below_udom_def)
 done
 
 text {* Universal domain is pointed *}
@@ -359,9 +359,9 @@
     assume "y \<in> insert a A" and "(if x \<sqsubseteq> a then a else x) \<sqsubseteq> y"
     thus "(if x \<sqsubseteq> a then a else x) = y"
       apply auto
-      apply (frule (1) trans_less)
+      apply (frule (1) below_trans)
       apply (frule (1) x_eq)
-      apply (rule antisym_less, assumption)
+      apply (rule below_antisym, assumption)
       apply simp
       apply (erule (1) x_eq)
       done
@@ -503,7 +503,7 @@
 done
 
 lemma rank_leD: "rank x \<le> n \<Longrightarrow> cb_take n x = x"
-apply (rule antisym_less [OF cb_take_less])
+apply (rule below_antisym [OF cb_take_less])
 apply (subst compact_approx_rank [symmetric])
 apply (erule cb_take_chain_le)
 done
@@ -727,7 +727,7 @@
       apply (rule IH)
        apply (simp add: less_max_iff_disj)
        apply (erule place_sub_less)
-      apply (erule rev_trans_less)
+      apply (erule rev_below_trans)
       apply (rule sub_below)
       done
   qed
@@ -779,9 +779,9 @@
 
 lemma basis_prj_mono: "ubasis_le a b \<Longrightarrow> basis_prj a \<sqsubseteq> basis_prj b"
 proof (induct a b rule: ubasis_le.induct)
-  case (ubasis_le_refl a) show ?case by (rule refl_less)
+  case (ubasis_le_refl a) show ?case by (rule below_refl)
 next
-  case (ubasis_le_trans a b c) thus ?case by - (rule trans_less)
+  case (ubasis_le_trans a b c) thus ?case by - (rule below_trans)
 next
   case (ubasis_le_lower S a i) thus ?case
     apply (cases "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Up.thy	Fri May 08 16:19:51 2009 -0700
@@ -26,11 +26,11 @@
 
 subsection {* Ordering on lifted cpo *}
 
-instantiation u :: (cpo) sq_ord
+instantiation u :: (cpo) below
 begin
 
 definition
-  less_up_def:
+  below_up_def:
     "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow>
       (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))"
 
@@ -38,13 +38,13 @@
 end
 
 lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
-by (simp add: less_up_def)
+by (simp add: below_up_def)
 
-lemma not_Iup_less [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
-by (simp add: less_up_def)
+lemma not_Iup_below [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
+by (simp add: below_up_def)
 
-lemma Iup_less [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
-by (simp add: less_up_def)
+lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
+by (simp add: below_up_def)
 
 subsection {* Lifted cpo is a partial order *}
 
@@ -52,17 +52,17 @@
 proof
   fix x :: "'a u"
   show "x \<sqsubseteq> x"
-    unfolding less_up_def by (simp split: u.split)
+    unfolding below_up_def by (simp split: u.split)
 next
   fix x y :: "'a u"
   assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
-    unfolding less_up_def
-    by (auto split: u.split_asm intro: antisym_less)
+    unfolding below_up_def
+    by (auto split: u.split_asm intro: below_antisym)
 next
   fix x y z :: "'a u"
   assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
-    unfolding less_up_def
-    by (auto split: u.split_asm intro: trans_less)
+    unfolding below_up_def
+    by (auto split: u.split_asm intro: below_trans)
 qed
 
 lemma u_UNIV: "UNIV = insert Ibottom (range Iup)"
@@ -78,7 +78,7 @@
   "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
 apply (rule is_lubI)
 apply (rule ub_rangeI)
-apply (subst Iup_less)
+apply (subst Iup_below)
 apply (erule is_ub_lub)
 apply (case_tac u)
 apply (drule ub_rangeD)
@@ -112,7 +112,7 @@
 lemma up_lemma4:
   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> chain (\<lambda>i. THE a. Iup a = Y (i + j))"
 apply (rule chainI)
-apply (rule Iup_less [THEN iffD1])
+apply (rule Iup_below [THEN iffD1])
 apply (subst up_lemma3, assumption+)+
 apply (simp add: chainE)
 done
@@ -235,9 +235,9 @@
 by (simp add: up_def cont_Iup inst_up_pcpo)
 
 lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
-by simp
+by simp (* FIXME: remove? *)
 
-lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
+lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
 by (simp add: up_def cont_Iup)
 
 lemma upE [cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
diff -r a9d6cf6de9a8 -r 99fe356cbbc2 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/UpperPD.thy	Fri May 08 16:19:51 2009 -0700
@@ -23,7 +23,7 @@
 apply (drule (1) bspec, erule bexE)
 apply (drule (1) bspec, erule bexE)
 apply (erule rev_bexI)
-apply (erule (1) trans_less)
+apply (erule (1) below_trans)
 done
 
 interpretation upper_le: preorder upper_le
@@ -38,7 +38,7 @@
 lemma PDPlus_upper_mono: "\<lbrakk>s \<le>\<sharp> t; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<sharp> PDPlus t v"
 unfolding upper_le_def Rep_PDPlus by fast
 
-lemma PDPlus_upper_less: "PDPlus t u \<le>\<sharp> t"
+lemma PDPlus_upper_le: "PDPlus t u \<le>\<sharp> t"
 unfolding upper_le_def Rep_PDPlus by fast
 
 lemma upper_le_PDUnit_PDUnit_iff [simp]:
@@ -97,7 +97,7 @@
   "{S::'a pd_basis set. upper_le.ideal S}"
 by (fast intro: upper_le.ideal_principal)
 
-instantiation upper_pd :: (profinite) sq_ord
+instantiation upper_pd :: (profinite) below
 begin
 
 definition
@@ -108,16 +108,16 @@
 
 instance upper_pd :: (profinite) po
 by (rule upper_le.typedef_ideal_po
-    [OF type_definition_upper_pd sq_le_upper_pd_def])
+    [OF type_definition_upper_pd below_upper_pd_def])
 
 instance upper_pd :: (profinite) cpo
 by (rule upper_le.typedef_ideal_cpo
-    [OF type_definition_upper_pd sq_le_upper_pd_def])
+    [OF type_definition_upper_pd below_upper_pd_def])
 
 lemma Rep_upper_pd_lub:
   "chain Y \<Longrightarrow> Rep_upper_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_upper_pd (Y i))"
 by (rule upper_le.typedef_ideal_rep_contlub
-    [OF type_definition_upper_pd sq_le_upper_pd_def])
+    [OF type_definition_upper_pd below_upper_pd_def])
 
 lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd xs)"
 by (rule Rep_upper_pd [unfolded mem_Collect_eq])
@@ -143,7 +143,7 @@
 apply (rule ideal_Rep_upper_pd)
 apply (erule Rep_upper_pd_lub)
 apply (rule Rep_upper_principal)
-apply (simp only: sq_le_upper_pd_def)
+apply (simp only: below_upper_pd_def)
 done
 
 text {* Upper powerdomain is pointed *}
@@ -262,28 +262,28 @@
 lemmas upper_plus_aci =
   upper_plus_ac upper_plus_absorb upper_plus_left_absorb
 
-lemma upper_plus_less1: "xs +\<sharp> ys \<sqsubseteq> xs"
+lemma upper_plus_below1: "xs +\<sharp> ys \<sqsubseteq> xs"
 apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
-apply (simp add: PDPlus_upper_less)
+apply (simp add: PDPlus_upper_le)
 done
 
-lemma upper_plus_less2: "xs +\<sharp> ys \<sqsubseteq> ys"
-by (subst upper_plus_commute, rule upper_plus_less1)
+lemma upper_plus_below2: "xs +\<sharp> ys \<sqsubseteq> ys"
+by (subst upper_plus_commute, rule upper_plus_below1)
 
 lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys +\<sharp> zs"
 apply (subst upper_plus_absorb [of xs, symmetric])
 apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
 done
 
-lemma upper_less_plus_iff:
+lemma upper_below_plus_iff:
   "xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
 apply safe
-apply (erule trans_less [OF _ upper_plus_less1])
-apply (erule trans_less [OF _ upper_plus_less2])
+apply (erule below_trans [OF _ upper_plus_below1])
+apply (erule below_trans [OF _ upper_plus_below2])
 apply (erule (1) upper_plus_greatest)
 done
 
-lemma upper_plus_less_unit_iff:
+lemma upper_plus_below_unit_iff:
   "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
  apply (rule iffI)
   apply (subgoal_tac
@@ -297,13 +297,13 @@
    apply simp
   apply simp
  apply (erule disjE)
-  apply (erule trans_less [OF upper_plus_less1])
- apply (erule trans_less [OF upper_plus_less2])
+  apply (erule below_trans [OF upper_plus_below1])
+ apply (erule below_trans [OF upper_plus_below2])
 done
 
-lemma upper_unit_less_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
+lemma upper_unit_below_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
  apply (rule iffI)
-  apply (rule profinite_less_ext)
+  apply (rule profinite_below_ext)
   apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
@@ -311,10 +311,10 @@
  apply (erule monofun_cfun_arg)
 done
 
-lemmas upper_pd_less_simps =
-  upper_unit_less_iff
-  upper_less_plus_iff
-  upper_plus_less_unit_iff
+lemmas upper_pd_below_simps =
+  upper_unit_below_iff
+  upper_below_plus_iff
+  upper_plus_below_unit_iff
 
 lemma upper_unit_eq_iff [simp]: "{x}\<sharp> = {y}\<sharp> \<longleftrightarrow> x = y"
 unfolding po_eq_conv by simp
@@ -323,10 +323,10 @@
 unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp
 
 lemma upper_plus_strict1 [simp]: "\<bottom> +\<sharp> ys = \<bottom>"
-by (rule UU_I, rule upper_plus_less1)
+by (rule UU_I, rule upper_plus_below1)
 
 lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
-by (rule UU_I, rule upper_plus_less2)
+by (rule UU_I, rule upper_plus_below2)
 
 lemma upper_unit_strict_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
 unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
@@ -407,11 +407,11 @@
 
 lemma upper_bind_basis_mono:
   "t \<le>\<sharp> u \<Longrightarrow> upper_bind_basis t \<sqsubseteq> upper_bind_basis u"
-unfolding expand_cfun_less
+unfolding expand_cfun_below
 apply (erule upper_le_induct, safe)
 apply (simp add: monofun_cfun)
-apply (simp add: trans_less [OF upper_plus_less1])
-apply (simp add: upper_less_plus_iff)
+apply (simp add: below_trans [OF upper_plus_below1])
+apply (simp add: upper_below_plus_iff)
 done
 
 definition