--- 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"