--- a/src/HOL/Lattice/CompleteLattice.thy Wed Dec 30 18:03:23 2015 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy Wed Dec 30 18:07:10 2015 +0100
@@ -31,15 +31,11 @@
*}
definition
- Meet :: "'a::complete_lattice set \<Rightarrow> 'a" where
- "Meet A = (THE inf. is_Inf A inf)"
+ Meet :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90) where
+ "\<Sqinter>A = (THE inf. is_Inf A inf)"
definition
- Join :: "'a::complete_lattice set \<Rightarrow> 'a" where
- "Join A = (THE sup. is_Sup A sup)"
-
-notation (xsymbols)
- Meet ("\<Sqinter>_" [90] 90) and
- Join ("\<Squnion>_" [90] 90)
+ Join :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90) where
+ "\<Squnion>A = (THE sup. is_Sup A sup)"
text {*
Due to unique existence of bounds, the complete lattice operations
--- a/src/HOL/Lattice/Lattice.thy Wed Dec 30 18:03:23 2015 +0100
+++ b/src/HOL/Lattice/Lattice.thy Wed Dec 30 18:07:10 2015 +0100
@@ -24,15 +24,11 @@
*}
definition
- meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "&&" 70) where
- "x && y = (THE inf. is_inf x y inf)"
+ meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) where
+ "x \<sqinter> y = (THE inf. is_inf x y inf)"
definition
- join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "||" 65) where
- "x || y = (THE sup. is_sup x y sup)"
-
-notation (xsymbols)
- meet (infixl "\<sqinter>" 70) and
- join (infixl "\<squnion>" 65)
+ join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) where
+ "x \<squnion> y = (THE sup. is_sup x y sup)"
text {*
Due to unique existence of bounds, the lattice operations may be
--- a/src/HOL/Lattice/Orders.thy Wed Dec 30 18:03:23 2015 +0100
+++ b/src/HOL/Lattice/Orders.thy Wed Dec 30 18:07:10 2015 +0100
@@ -18,10 +18,7 @@
*}
class leq =
- fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "[=" 50)
-
-notation (xsymbols)
- leq (infixl "\<sqsubseteq>" 50)
+ fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
class quasi_order = leq +
assumes leq_refl [intro?]: "x \<sqsubseteq> x"