--- a/src/HOL/Complete_Lattices.thy Wed Sep 12 20:58:06 2018 +0200
+++ b/src/HOL/Complete_Lattices.thy Wed Sep 12 22:33:26 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}"
--- a/src/HOL/Lattices_Big.thy Wed Sep 12 20:58:06 2018 +0200
+++ b/src/HOL/Lattices_Big.thy Wed Sep 12 22:33:26 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
--- a/src/HOL/Library/Complete_Partial_Order2.thy Wed Sep 12 20:58:06 2018 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Wed Sep 12 22:33:26 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)"
--- a/src/HOL/Library/Lattice_Syntax.thy Wed Sep 12 20:58:06 2018 +0200
+++ b/src/HOL/Library/Lattice_Syntax.thy Wed Sep 12 22:33:26 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)
--- a/src/HOL/Library/Multiset.thy Wed Sep 12 20:58:06 2018 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Sep 12 22:33:26 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>
--- a/src/HOL/Library/Option_ord.thy Wed Sep 12 20:58:06 2018 +0200
+++ b/src/HOL/Library/Option_ord.thy Wed Sep 12 22:33:26 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)
--- a/src/HOL/Main.thy Wed Sep 12 20:58:06 2018 +0200
+++ b/src/HOL/Main.thy Wed Sep 12 22:33:26 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