# HG changeset patch
# User huffman
# Date 1288995328 25200
# Node ID adb22dbb5242d2b93ebe0ca53b6642c5114533a3
# Parent  a26503ac7c877c8befa8c940139b56ba3d995f52
(infixl "<<" 55) -> (infix "<<" 50)

diff -r a26503ac7c87 -r adb22dbb5242 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Wed Nov 03 17:22:25 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy	Fri Nov 05 15:15:28 2010 -0700
@@ -33,7 +33,7 @@
 unfolding convex_le_def by (fast intro: PDPlus_upper_mono PDPlus_lower_mono)
 
 lemma convex_le_PDUnit_PDUnit_iff [simp]:
-  "(PDUnit a \<le>\<natural> PDUnit b) = a \<sqsubseteq> b"
+  "(PDUnit a \<le>\<natural> PDUnit b) = (a \<sqsubseteq> b)"
 unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit by fast
 
 lemma convex_le_PDUnit_lemma1:
diff -r a26503ac7c87 -r adb22dbb5242 src/HOLCF/Library/Sum_Cpo.thy
--- a/src/HOLCF/Library/Sum_Cpo.thy	Wed Nov 03 17:22:25 2010 -0700
+++ b/src/HOLCF/Library/Sum_Cpo.thy	Fri Nov 05 15:15:28 2010 -0700
@@ -21,10 +21,10 @@
 instance ..
 end
 
-lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
+lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y \<longleftrightarrow> x \<sqsubseteq> y"
 unfolding below_sum_def by simp
 
-lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
+lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y \<longleftrightarrow> x \<sqsubseteq> y"
 unfolding below_sum_def by simp
 
 lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
diff -r a26503ac7c87 -r adb22dbb5242 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Wed Nov 03 17:22:25 2010 -0700
+++ b/src/HOLCF/LowerPD.thy	Fri Nov 05 15:15:28 2010 -0700
@@ -43,7 +43,7 @@
 unfolding lower_le_def Rep_PDPlus by fast
 
 lemma lower_le_PDUnit_PDUnit_iff [simp]:
-  "(PDUnit a \<le>\<flat> PDUnit b) = a \<sqsubseteq> b"
+  "(PDUnit a \<le>\<flat> PDUnit b) = (a \<sqsubseteq> b)"
 unfolding lower_le_def Rep_PDUnit by fast
 
 lemma lower_le_PDUnit_PDPlus_iff:
diff -r a26503ac7c87 -r adb22dbb5242 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Wed Nov 03 17:22:25 2010 -0700
+++ b/src/HOLCF/Porder.thy	Fri Nov 05 15:15:28 2010 -0700
@@ -15,10 +15,10 @@
 begin
 
 notation
-  below (infixl "<<" 55)
+  below (infix "<<" 50)
 
 notation (xsymbols)
-  below (infixl "\<sqsubseteq>" 55)
+  below (infix "\<sqsubseteq>" 50)
 
 lemma below_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
   by (rule subst)
@@ -62,7 +62,7 @@
 
 subsection {* Upper bounds *}
 
-definition is_ub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<|" 55) where
+definition is_ub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<|" 55) where
   "S <| x \<longleftrightarrow> (\<forall>y\<in>S. y \<sqsubseteq> x)"
 
 lemma is_ubI: "(\<And>x. x \<in> S \<Longrightarrow> x \<sqsubseteq> u) \<Longrightarrow> S <| u"
@@ -94,7 +94,7 @@
 
 subsection {* Least upper bounds *}
 
-definition is_lub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<<|" 55) where
+definition is_lub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<<|" 55) where
   "S <<| x \<longleftrightarrow> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)"
 
 definition lub :: "'a set \<Rightarrow> 'a" where
diff -r a26503ac7c87 -r adb22dbb5242 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Wed Nov 03 17:22:25 2010 -0700
+++ b/src/HOLCF/Sprod.thy	Fri Nov 05 15:15:28 2010 -0700
@@ -151,18 +151,18 @@
 lemma spair_sfst_ssnd: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
 by (cases p, simp_all)
 
-lemma below_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
+lemma below_sprod: "(x \<sqsubseteq> y) = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
 by (simp add: Rep_sprod_simps sfst_def ssnd_def cont_Rep_sprod)
 
 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 below_sprod)
 
-lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
+lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
 apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
 apply (simp add: below_sprod)
 done
 
-lemma ssnd_below_iff: "ssnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:sfst\<cdot>x, y:)"
+lemma ssnd_below_iff: "ssnd\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (:sfst\<cdot>x, y:)"
 apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
 apply (simp add: below_sprod)
 done
diff -r a26503ac7c87 -r adb22dbb5242 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Wed Nov 03 17:22:25 2010 -0700
+++ b/src/HOLCF/UpperPD.thy	Fri Nov 05 15:15:28 2010 -0700
@@ -42,7 +42,7 @@
 unfolding upper_le_def Rep_PDPlus by fast
 
 lemma upper_le_PDUnit_PDUnit_iff [simp]:
-  "(PDUnit a \<le>\<sharp> PDUnit b) = a \<sqsubseteq> b"
+  "(PDUnit a \<le>\<sharp> PDUnit b) = (a \<sqsubseteq> b)"
 unfolding upper_le_def Rep_PDUnit by fast
 
 lemma upper_le_PDPlus_PDUnit_iff: