--- a/src/HOL/Complete_Lattices.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Complete_Lattices.thy Mon Dec 28 17:43:30 2015 +0100
@@ -901,12 +901,9 @@
subsubsection \<open>Inter\<close>
-abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
- "Inter S \<equiv> \<Sqinter>S"
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set" ("\<Inter>_" [900] 900)
+ where "\<Inter>S \<equiv> \<Sqinter>S"
-notation (xsymbols)
- Inter ("\<Inter>_" [900] 900)
-
lemma Inter_eq:
"\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
proof (rule set_eqI)
@@ -944,7 +941,7 @@
"(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
by (fact Inf_less_eq)
-lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> Inter A"
+lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> \<Inter>A"
by (fact Inf_greatest)
lemma Inter_empty: "\<Inter>{} = UNIV"
@@ -1080,11 +1077,8 @@
subsubsection \<open>Union\<close>
-abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
- "Union S \<equiv> \<Squnion>S"
-
-notation (xsymbols)
- Union ("\<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}"