# HG changeset patch
# User wenzelm
# Date 1451495230 -3600
# Node ID 8fb53badad9923c5da181040f06129b616e4bb59
# Parent  3af5a06577c70f8da51c325f52f77e920f9cdb97
more symbols;

diff -r 3af5a06577c7 -r 8fb53badad99 src/HOL/Lattice/CompleteLattice.thy
--- 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
diff -r 3af5a06577c7 -r 8fb53badad99 src/HOL/Lattice/Lattice.thy
--- 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
diff -r 3af5a06577c7 -r 8fb53badad99 src/HOL/Lattice/Orders.thy
--- 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"