added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
authornipkow
Wed Sep 12 18:44:31 2018 +0200 (11 months ago)
changeset 689805717fbc55521
parent 68979 e2244e5707dd
child 68982 807099160468
child 68983 caedabd2771c
added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
src/HOL/Complete_Lattices.thy
src/HOL/Lattices_Big.thy
src/HOL/Library/Complete_Partial_Order2.thy
src/HOL/Library/Lattice_Syntax.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Option_ord.thy
src/HOL/Main.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Wed Sep 12 17:12:33 2018 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Wed Sep 12 18:44:31 2018 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  subsection \<open>Syntactic infimum and supremum operations\<close>
     1.5  
     1.6  class Inf =
     1.7 -  fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter>_" [900] 900)
     1.8 +  fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter> _" [900] 900)
     1.9  begin
    1.10  
    1.11  abbreviation (input) INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
    1.12 @@ -24,7 +24,7 @@
    1.13  end
    1.14  
    1.15  class Sup =
    1.16 -  fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion>_" [900] 900)
    1.17 +  fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion> _" [900] 900)
    1.18  begin
    1.19  
    1.20  abbreviation (input) SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
    1.21 @@ -791,7 +791,7 @@
    1.22  
    1.23  subsubsection \<open>Inter\<close>
    1.24  
    1.25 -abbreviation Inter :: "'a set set \<Rightarrow> 'a set"  ("\<Inter>_" [900] 900)
    1.26 +abbreviation Inter :: "'a set set \<Rightarrow> 'a set"  ("\<Inter> _" [900] 900)
    1.27    where "\<Inter>S \<equiv> \<Sqinter>S"
    1.28  
    1.29  lemma Inter_eq: "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
    1.30 @@ -948,7 +948,7 @@
    1.31  
    1.32  subsubsection \<open>Union\<close>
    1.33  
    1.34 -abbreviation Union :: "'a set set \<Rightarrow> 'a set"  ("\<Union>_" [900] 900)
    1.35 +abbreviation Union :: "'a set set \<Rightarrow> 'a set"  ("\<Union> _" [900] 900)
    1.36    where "\<Union>S \<equiv> \<Squnion>S"
    1.37  
    1.38  lemma Union_eq: "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
     2.1 --- a/src/HOL/Lattices_Big.thy	Wed Sep 12 17:12:33 2018 +0100
     2.2 +++ b/src/HOL/Lattices_Big.thy	Wed Sep 12 18:44:31 2018 +0200
     2.3 @@ -309,7 +309,7 @@
     2.4  
     2.5  sublocale Inf_fin: semilattice_order_set inf less_eq less
     2.6  defines
     2.7 -  Inf_fin ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Inf_fin.F ..
     2.8 +  Inf_fin ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Inf_fin.F ..
     2.9  
    2.10  end
    2.11  
    2.12 @@ -318,7 +318,7 @@
    2.13  
    2.14  sublocale Sup_fin: semilattice_order_set sup greater_eq greater
    2.15  defines
    2.16 -  Sup_fin ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Sup_fin.F ..
    2.17 +  Sup_fin ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Sup_fin.F ..
    2.18  
    2.19  end
    2.20  
     3.1 --- a/src/HOL/Library/Complete_Partial_Order2.thy	Wed Sep 12 17:12:33 2018 +0100
     3.2 +++ b/src/HOL/Library/Complete_Partial_Order2.thy	Wed Sep 12 18:44:31 2018 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4    includes lifting_syntax
     3.5    shows "((A ===> A ===> (=)) ===> rel_set A ===> (=)) Complete_Partial_Order.chain Complete_Partial_Order.chain"
     3.6  unfolding chain_def[abs_def] by transfer_prover
     3.7 -
     3.8 +                             
     3.9  lemma linorder_chain [simp, intro!]:
    3.10    fixes Y :: "_ :: linorder set"
    3.11    shows "Complete_Partial_Order.chain (\<le>) Y"
    3.12 @@ -161,7 +161,7 @@
    3.13  end
    3.14  
    3.15  lemma Sup_image_mono_le:
    3.16 -  fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or>_" [900] 900)
    3.17 +  fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or> _" [900] 900)
    3.18    assumes ccpo: "class.ccpo Sup_b (\<sqsubseteq>) lt_b"
    3.19    assumes chain: "Complete_Partial_Order.chain (\<sqsubseteq>) Y"
    3.20    and mono: "\<And>x y. \<lbrakk> x \<sqsubseteq> y; x \<in> Y \<rbrakk> \<Longrightarrow> f x \<le> f y"
    3.21 @@ -556,7 +556,7 @@
    3.22  
    3.23  context
    3.24    fixes ord :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) 
    3.25 -  and lub :: "'b set \<Rightarrow> 'b" ("\<Or>_" [900] 900)
    3.26 +  and lub :: "'b set \<Rightarrow> 'b" ("\<Or> _" [900] 900)
    3.27  begin
    3.28  
    3.29  lemma cont_fun_lub_Sup:
    3.30 @@ -677,7 +677,7 @@
    3.31  by(rule monotoneI)(auto intro: bot intro: mono order_trans)
    3.32  
    3.33  lemma (in ccpo) mcont_if_bot:
    3.34 -  fixes bot and lub ("\<Or>_" [900] 900) and ord (infix "\<sqsubseteq>" 60)
    3.35 +  fixes bot and lub ("\<Or> _" [900] 900) and ord (infix "\<sqsubseteq>" 60)
    3.36    assumes ccpo: "class.ccpo lub (\<sqsubseteq>) lt"
    3.37    and mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
    3.38    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)"
    3.39 @@ -877,7 +877,7 @@
    3.40  end
    3.41  
    3.42  lemma admissible_leI:
    3.43 -  fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or>_" [900] 900)
    3.44 +  fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or> _" [900] 900)
    3.45    assumes "class.ccpo lub (\<sqsubseteq>) (mk_less (\<sqsubseteq>))"
    3.46    and "mcont luba orda lub (\<sqsubseteq>) (\<lambda>x. f x)"
    3.47    and "mcont luba orda lub (\<sqsubseteq>) (\<lambda>x. g x)"
     4.1 --- a/src/HOL/Library/Lattice_Syntax.thy	Wed Sep 12 17:12:33 2018 +0100
     4.2 +++ b/src/HOL/Library/Lattice_Syntax.thy	Wed Sep 12 18:44:31 2018 +0200
     4.3 @@ -11,8 +11,8 @@
     4.4    top ("\<top>") and
     4.5    inf  (infixl "\<sqinter>" 70) and
     4.6    sup  (infixl "\<squnion>" 65) and
     4.7 -  Inf  ("\<Sqinter>_" [900] 900) and
     4.8 -  Sup  ("\<Squnion>_" [900] 900)
     4.9 +  Inf  ("\<Sqinter> _" [900] 900) and
    4.10 +  Sup  ("\<Squnion> _" [900] 900)
    4.11  
    4.12  syntax
    4.13    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
     5.1 --- a/src/HOL/Library/Multiset.thy	Wed Sep 12 17:12:33 2018 +0100
     5.2 +++ b/src/HOL/Library/Multiset.thy	Wed Sep 12 18:44:31 2018 +0200
     5.3 @@ -2384,7 +2384,7 @@
     5.4    shows \<open>(\<Sum>x\<in>#A. y) = of_nat (size A) * y\<close>
     5.5    by (induction A) (auto simp: algebra_simps)
     5.6  
     5.7 -abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
     5.8 +abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union># _" [900] 900)
     5.9    where "\<Union># MM \<equiv> sum_mset MM" \<comment> \<open>FIXME ambiguous notation --
    5.10      could likewise refer to \<open>\<Squnion>#\<close>\<close>
    5.11  
     6.1 --- a/src/HOL/Library/Option_ord.thy	Wed Sep 12 17:12:33 2018 +0100
     6.2 +++ b/src/HOL/Library/Option_ord.thy	Wed Sep 12 18:44:31 2018 +0200
     6.3 @@ -13,8 +13,8 @@
     6.4    top ("\<top>") and
     6.5    inf  (infixl "\<sqinter>" 70) and
     6.6    sup  (infixl "\<squnion>" 65) and
     6.7 -  Inf  ("\<Sqinter>_" [900] 900) and
     6.8 -  Sup  ("\<Squnion>_" [900] 900)
     6.9 +  Inf  ("\<Sqinter> _" [900] 900) and
    6.10 +  Sup  ("\<Squnion> _" [900] 900)
    6.11  
    6.12  syntax
    6.13    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    6.14 @@ -466,8 +466,8 @@
    6.15    top ("\<top>") and
    6.16    inf  (infixl "\<sqinter>" 70) and
    6.17    sup  (infixl "\<squnion>" 65) and
    6.18 -  Inf  ("\<Sqinter>_" [900] 900) and
    6.19 -  Sup  ("\<Squnion>_" [900] 900)
    6.20 +  Inf  ("\<Sqinter> _" [900] 900) and
    6.21 +  Sup  ("\<Squnion> _" [900] 900)
    6.22  
    6.23  no_syntax
    6.24    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
     7.1 --- a/src/HOL/Main.thy	Wed Sep 12 17:12:33 2018 +0100
     7.2 +++ b/src/HOL/Main.thy	Wed Sep 12 18:44:31 2018 +0200
     7.3 @@ -22,8 +22,8 @@
     7.4    top ("\<top>") and
     7.5    inf (infixl "\<sqinter>" 70) and
     7.6    sup (infixl "\<squnion>" 65) and
     7.7 -  Inf ("\<Sqinter>_" [900] 900) and
     7.8 -  Sup ("\<Squnion>_" [900] 900) and
     7.9 +  Inf ("\<Sqinter> _" [900] 900) and
    7.10 +  Sup ("\<Squnion> _" [900] 900) and
    7.11    ordLeq2 (infix "<=o" 50) and
    7.12    ordLeq3 (infix "\<le>o" 50) and
    7.13    ordLess2 (infix "<o" 50) and