diff -r f2bb6541f532 -r ad093e4638e2 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Thu Dec 23 12:20:09 2010 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy	Thu Dec 23 11:51:59 2010 -0800
@@ -132,14 +132,14 @@
 
 abbreviation
   lower_add :: "'a lower_pd \<Rightarrow> 'a lower_pd \<Rightarrow> 'a lower_pd"
-    (infixl "+\<flat>" 65) where
-  "xs +\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
+    (infixl "\<union>\<flat>" 65) where
+  "xs \<union>\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
 
 syntax
   "_lower_pd" :: "args \<Rightarrow> 'a lower_pd" ("{_}\<flat>")
 
 translations
-  "{x,xs}\<flat>" == "{x}\<flat> +\<flat> {xs}\<flat>"
+  "{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>"
   "{x}\<flat>" == "CONST lower_unit\<cdot>x"
 
 lemma lower_unit_Rep_compact_basis [simp]:
@@ -148,23 +148,23 @@
 by (simp add: compact_basis.extension_principal PDUnit_lower_mono)
 
 lemma lower_plus_principal [simp]:
-  "lower_principal t +\<flat> lower_principal u = lower_principal (PDPlus t u)"
+  "lower_principal t \<union>\<flat> lower_principal u = lower_principal (PDPlus t u)"
 unfolding lower_plus_def
 by (simp add: lower_pd.extension_principal
     lower_pd.extension_mono PDPlus_lower_mono)
 
 interpretation lower_add: semilattice lower_add proof
   fix xs ys zs :: "'a lower_pd"
-  show "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
+  show "(xs \<union>\<flat> ys) \<union>\<flat> zs = xs \<union>\<flat> (ys \<union>\<flat> zs)"
     apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
     apply (rule_tac x=zs in lower_pd.principal_induct, simp)
     apply (simp add: PDPlus_assoc)
     done
-  show "xs +\<flat> ys = ys +\<flat> xs"
+  show "xs \<union>\<flat> ys = ys \<union>\<flat> xs"
     apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
     apply (simp add: PDPlus_commute)
     done
-  show "xs +\<flat> xs = xs"
+  show "xs \<union>\<flat> xs = xs"
     apply (induct xs rule: lower_pd.principal_induct, simp)
     apply (simp add: PDPlus_absorb)
     done
@@ -184,21 +184,21 @@
 lemmas lower_plus_aci =
   lower_plus_ac lower_plus_absorb lower_plus_left_absorb
 
-lemma lower_plus_below1: "xs \<sqsubseteq> xs +\<flat> ys"
+lemma lower_plus_below1: "xs \<sqsubseteq> xs \<union>\<flat> ys"
 apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
 apply (simp add: PDPlus_lower_le)
 done
 
-lemma lower_plus_below2: "ys \<sqsubseteq> xs +\<flat> ys"
+lemma lower_plus_below2: "ys \<sqsubseteq> xs \<union>\<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"
+lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<union>\<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_below_iff [simp]:
-  "xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
+  "xs \<union>\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
 apply safe
 apply (erule below_trans [OF lower_plus_below1])
 apply (erule below_trans [OF lower_plus_below2])
@@ -206,7 +206,7 @@
 done
 
 lemma lower_unit_below_plus_iff [simp]:
-  "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
+  "{x}\<flat> \<sqsubseteq> ys \<union>\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
 apply (induct x rule: compact_basis.principal_induct, simp)
 apply (induct ys rule: lower_pd.principal_induct, simp)
 apply (induct zs rule: lower_pd.principal_induct, simp)
@@ -235,19 +235,19 @@
 unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
 
 lemma lower_plus_bottom_iff [simp]:
-  "xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
+  "xs \<union>\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
 apply safe
 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"
+lemma lower_plus_strict1 [simp]: "\<bottom> \<union>\<flat> ys = ys"
 apply (rule below_antisym [OF _ lower_plus_below2])
 apply (simp add: lower_plus_least)
 done
 
-lemma lower_plus_strict2 [simp]: "xs +\<flat> \<bottom> = xs"
+lemma lower_plus_strict2 [simp]: "xs \<union>\<flat> \<bottom> = xs"
 apply (rule below_antisym [OF _ lower_plus_below1])
 apply (simp add: lower_plus_least)
 done
@@ -262,7 +262,7 @@
 done
 
 lemma compact_lower_plus [simp]:
-  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<flat> ys)"
+  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<flat> ys)"
 by (auto dest!: lower_pd.compact_imp_principal)
 
 
@@ -272,7 +272,7 @@
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<flat>"
   assumes insert:
-    "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> +\<flat> ys)"
+    "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> \<union>\<flat> ys)"
   shows "P (xs::'a lower_pd)"
 apply (induct xs rule: lower_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct1)
@@ -287,7 +287,7 @@
   [case_names adm lower_unit lower_plus, induct type: lower_pd]:
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<flat>"
-  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<flat> ys)"
+  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<flat> ys)"
   shows "P (xs::'a lower_pd)"
 apply (induct xs rule: lower_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct)
@@ -303,10 +303,10 @@
   "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
   "lower_bind_basis = fold_pd
     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
-    (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
+    (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)"
 
 lemma ACI_lower_bind:
-  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
+  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)"
 apply unfold_locales
 apply (simp add: lower_plus_assoc)
 apply (simp add: lower_plus_commute)
@@ -317,7 +317,7 @@
   "lower_bind_basis (PDUnit a) =
     (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   "lower_bind_basis (PDPlus t u) =
-    (\<Lambda> f. lower_bind_basis t\<cdot>f +\<flat> lower_bind_basis u\<cdot>f)"
+    (\<Lambda> f. lower_bind_basis t\<cdot>f \<union>\<flat> lower_bind_basis u\<cdot>f)"
 unfolding lower_bind_basis_def
 apply -
 apply (rule fold_pd_PDUnit [OF ACI_lower_bind])
@@ -356,7 +356,7 @@
 by (induct x rule: compact_basis.principal_induct, simp, simp)
 
 lemma lower_bind_plus [simp]:
-  "lower_bind\<cdot>(xs +\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f +\<flat> lower_bind\<cdot>ys\<cdot>f"
+  "lower_bind\<cdot>(xs \<union>\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f \<union>\<flat> lower_bind\<cdot>ys\<cdot>f"
 by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
 
 lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
@@ -378,7 +378,7 @@
 unfolding lower_map_def by simp
 
 lemma lower_map_plus [simp]:
-  "lower_map\<cdot>f\<cdot>(xs +\<flat> ys) = lower_map\<cdot>f\<cdot>xs +\<flat> lower_map\<cdot>f\<cdot>ys"
+  "lower_map\<cdot>f\<cdot>(xs \<union>\<flat> ys) = lower_map\<cdot>f\<cdot>xs \<union>\<flat> lower_map\<cdot>f\<cdot>ys"
 unfolding lower_map_def by simp
 
 lemma lower_map_bottom [simp]: "lower_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<flat>"
@@ -484,7 +484,7 @@
 unfolding lower_join_def by simp
 
 lemma lower_join_plus [simp]:
-  "lower_join\<cdot>(xss +\<flat> yss) = lower_join\<cdot>xss +\<flat> lower_join\<cdot>yss"
+  "lower_join\<cdot>(xss \<union>\<flat> yss) = lower_join\<cdot>xss \<union>\<flat> lower_join\<cdot>yss"
 unfolding lower_join_def by simp
 
 lemma lower_join_bottom [simp]: "lower_join\<cdot>\<bottom> = \<bottom>"