# HG changeset patch
# User nipkow
# Date 1536770671 -7200
# Node ID 5717fbc555219b286d14fb770bc161fbbd3feea1
# Parent  e2244e5707dd9ab809c753defbef24ce658d3b73
added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x

diff -r e2244e5707dd -r 5717fbc55521 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Wed Sep 12 17:12:33 2018 +0100
+++ b/src/HOL/Complete_Lattices.thy	Wed Sep 12 18:44:31 2018 +0200
@@ -15,7 +15,7 @@
 subsection \<open>Syntactic infimum and supremum operations\<close>
 
 class Inf =
-  fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter>_" [900] 900)
+  fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter> _" [900] 900)
 begin
 
 abbreviation (input) INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
@@ -24,7 +24,7 @@
 end
 
 class Sup =
-  fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion>_" [900] 900)
+  fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion> _" [900] 900)
 begin
 
 abbreviation (input) SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
@@ -791,7 +791,7 @@
 
 subsubsection \<open>Inter\<close>
 
-abbreviation Inter :: "'a set set \<Rightarrow> 'a set"  ("\<Inter>_" [900] 900)
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set"  ("\<Inter> _" [900] 900)
   where "\<Inter>S \<equiv> \<Sqinter>S"
 
 lemma Inter_eq: "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
@@ -948,7 +948,7 @@
 
 subsubsection \<open>Union\<close>
 
-abbreviation Union :: "'a set set \<Rightarrow> 'a set"  ("\<Union>_" [900] 900)
+abbreviation Union :: "'a set set \<Rightarrow> 'a set"  ("\<Union> _" [900] 900)
   where "\<Union>S \<equiv> \<Squnion>S"
 
 lemma Union_eq: "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
diff -r e2244e5707dd -r 5717fbc55521 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Wed Sep 12 17:12:33 2018 +0100
+++ b/src/HOL/Lattices_Big.thy	Wed Sep 12 18:44:31 2018 +0200
@@ -309,7 +309,7 @@
 
 sublocale Inf_fin: semilattice_order_set inf less_eq less
 defines
-  Inf_fin ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Inf_fin.F ..
+  Inf_fin ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Inf_fin.F ..
 
 end
 
@@ -318,7 +318,7 @@
 
 sublocale Sup_fin: semilattice_order_set sup greater_eq greater
 defines
-  Sup_fin ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Sup_fin.F ..
+  Sup_fin ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Sup_fin.F ..
 
 end
 
diff -r e2244e5707dd -r 5717fbc55521 src/HOL/Library/Complete_Partial_Order2.thy
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Wed Sep 12 17:12:33 2018 +0100
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Wed Sep 12 18:44:31 2018 +0200
@@ -12,7 +12,7 @@
   includes lifting_syntax
   shows "((A ===> A ===> (=)) ===> rel_set A ===> (=)) Complete_Partial_Order.chain Complete_Partial_Order.chain"
 unfolding chain_def[abs_def] by transfer_prover
-
+                             
 lemma linorder_chain [simp, intro!]:
   fixes Y :: "_ :: linorder set"
   shows "Complete_Partial_Order.chain (\<le>) Y"
@@ -161,7 +161,7 @@
 end
 
 lemma Sup_image_mono_le:
-  fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or>_" [900] 900)
+  fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or> _" [900] 900)
   assumes ccpo: "class.ccpo Sup_b (\<sqsubseteq>) lt_b"
   assumes chain: "Complete_Partial_Order.chain (\<sqsubseteq>) Y"
   and mono: "\<And>x y. \<lbrakk> x \<sqsubseteq> y; x \<in> Y \<rbrakk> \<Longrightarrow> f x \<le> f y"
@@ -556,7 +556,7 @@
 
 context
   fixes ord :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) 
-  and lub :: "'b set \<Rightarrow> 'b" ("\<Or>_" [900] 900)
+  and lub :: "'b set \<Rightarrow> 'b" ("\<Or> _" [900] 900)
 begin
 
 lemma cont_fun_lub_Sup:
@@ -677,7 +677,7 @@
 by(rule monotoneI)(auto intro: bot intro: mono order_trans)
 
 lemma (in ccpo) mcont_if_bot:
-  fixes bot and lub ("\<Or>_" [900] 900) and ord (infix "\<sqsubseteq>" 60)
+  fixes bot and lub ("\<Or> _" [900] 900) and ord (infix "\<sqsubseteq>" 60)
   assumes ccpo: "class.ccpo lub (\<sqsubseteq>) lt"
   and mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
   and cont: "\<And>Y. \<lbrakk> Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}; \<And>x. x \<in> Y \<Longrightarrow> \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f (\<Squnion>Y) = \<Or>(f ` Y)"
@@ -877,7 +877,7 @@
 end
 
 lemma admissible_leI:
-  fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or>_" [900] 900)
+  fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or> _" [900] 900)
   assumes "class.ccpo lub (\<sqsubseteq>) (mk_less (\<sqsubseteq>))"
   and "mcont luba orda lub (\<sqsubseteq>) (\<lambda>x. f x)"
   and "mcont luba orda lub (\<sqsubseteq>) (\<lambda>x. g x)"
diff -r e2244e5707dd -r 5717fbc55521 src/HOL/Library/Lattice_Syntax.thy
--- a/src/HOL/Library/Lattice_Syntax.thy	Wed Sep 12 17:12:33 2018 +0100
+++ b/src/HOL/Library/Lattice_Syntax.thy	Wed Sep 12 18:44:31 2018 +0200
@@ -11,8 +11,8 @@
   top ("\<top>") and
   inf  (infixl "\<sqinter>" 70) and
   sup  (infixl "\<squnion>" 65) and
-  Inf  ("\<Sqinter>_" [900] 900) and
-  Sup  ("\<Squnion>_" [900] 900)
+  Inf  ("\<Sqinter> _" [900] 900) and
+  Sup  ("\<Squnion> _" [900] 900)
 
 syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
diff -r e2244e5707dd -r 5717fbc55521 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Sep 12 17:12:33 2018 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Sep 12 18:44:31 2018 +0200
@@ -2384,7 +2384,7 @@
   shows \<open>(\<Sum>x\<in>#A. y) = of_nat (size A) * y\<close>
   by (induction A) (auto simp: algebra_simps)
 
-abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
+abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union># _" [900] 900)
   where "\<Union># MM \<equiv> sum_mset MM" \<comment> \<open>FIXME ambiguous notation --
     could likewise refer to \<open>\<Squnion>#\<close>\<close>
 
diff -r e2244e5707dd -r 5717fbc55521 src/HOL/Library/Option_ord.thy
--- a/src/HOL/Library/Option_ord.thy	Wed Sep 12 17:12:33 2018 +0100
+++ b/src/HOL/Library/Option_ord.thy	Wed Sep 12 18:44:31 2018 +0200
@@ -13,8 +13,8 @@
   top ("\<top>") and
   inf  (infixl "\<sqinter>" 70) and
   sup  (infixl "\<squnion>" 65) and
-  Inf  ("\<Sqinter>_" [900] 900) and
-  Sup  ("\<Squnion>_" [900] 900)
+  Inf  ("\<Sqinter> _" [900] 900) and
+  Sup  ("\<Squnion> _" [900] 900)
 
 syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
@@ -466,8 +466,8 @@
   top ("\<top>") and
   inf  (infixl "\<sqinter>" 70) and
   sup  (infixl "\<squnion>" 65) and
-  Inf  ("\<Sqinter>_" [900] 900) and
-  Sup  ("\<Squnion>_" [900] 900)
+  Inf  ("\<Sqinter> _" [900] 900) and
+  Sup  ("\<Squnion> _" [900] 900)
 
 no_syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
diff -r e2244e5707dd -r 5717fbc55521 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Wed Sep 12 17:12:33 2018 +0100
+++ b/src/HOL/Main.thy	Wed Sep 12 18:44:31 2018 +0200
@@ -22,8 +22,8 @@
   top ("\<top>") and
   inf (infixl "\<sqinter>" 70) and
   sup (infixl "\<squnion>" 65) and
-  Inf ("\<Sqinter>_" [900] 900) and
-  Sup ("\<Squnion>_" [900] 900) and
+  Inf ("\<Sqinter> _" [900] 900) and
+  Sup ("\<Squnion> _" [900] 900) and
   ordLeq2 (infix "<=o" 50) and
   ordLeq3 (infix "\<le>o" 50) and
   ordLess2 (infix "<o" 50) and