# HG changeset patch
# User haftmann
# Date 1330283414 -3600
# Node ID 72d81e78910634c355963df9fcf5b7c556665a46
# Parent  07f9732804ad26d87b98b2b2b58788ab6291e4d2
tuned syntax declarations; tuned structure

diff -r 07f9732804ad -r 72d81e789106 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sun Feb 26 20:08:12 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy	Sun Feb 26 20:10:14 2012 +0100
@@ -8,11 +8,7 @@
 
 notation
   less_eq (infix "\<sqsubseteq>" 50) and
-  less (infix "\<sqsubset>" 50) and
-  inf (infixl "\<sqinter>" 70) and
-  sup (infixl "\<squnion>" 65) and
-  top ("\<top>") and
-  bot ("\<bottom>")
+  less (infix "\<sqsubset>" 50)
 
 
 subsection {* Syntactic infimum and supremum operations *}
@@ -23,6 +19,7 @@
 class Sup =
   fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
 
+
 subsection {* Abstract complete lattices *}
 
 class complete_lattice = bounded_lattice + Inf + Sup +
@@ -1214,14 +1211,8 @@
 text {* Finally *}
 
 no_notation
-  less_eq  (infix "\<sqsubseteq>" 50) and
-  less (infix "\<sqsubset>" 50) and
-  bot ("\<bottom>") and
-  top ("\<top>") and
-  inf  (infixl "\<sqinter>" 70) and
-  sup  (infixl "\<squnion>" 65) and
-  Inf  ("\<Sqinter>_" [900] 900) and
-  Sup  ("\<Squnion>_" [900] 900)
+  less_eq (infix "\<sqsubseteq>" 50) and
+  less (infix "\<sqsubset>" 50)
 
 no_syntax (xsymbols)
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
diff -r 07f9732804ad -r 72d81e789106 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sun Feb 26 20:08:12 2012 +0100
+++ b/src/HOL/Lattices.thy	Sun Feb 26 20:10:14 2012 +0100
@@ -43,13 +43,7 @@
 end
 
 
-subsection {* Concrete lattices *}
-
-notation
-  less_eq  (infix "\<sqsubseteq>" 50) and
-  less  (infix "\<sqsubset>" 50) and
-  bot ("\<bottom>") and
-  top ("\<top>")
+subsection {* Syntactic infimum and supremum operations *}
 
 class inf =
   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
@@ -57,6 +51,13 @@
 class sup = 
   fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
 
+
+subsection {* Concrete lattices *}
+
+notation
+  less_eq  (infix "\<sqsubseteq>" 50) and
+  less  (infix "\<sqsubset>" 50)
+
 class semilattice_inf =  order + inf +
   assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
   and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
@@ -759,12 +760,8 @@
 
 
 no_notation
-  less_eq  (infix "\<sqsubseteq>" 50) and
-  less (infix "\<sqsubset>" 50) and
-  inf  (infixl "\<sqinter>" 70) and
-  sup  (infixl "\<squnion>" 65) and
-  top ("\<top>") and
-  bot ("\<bottom>")
+  less_eq (infix "\<sqsubseteq>" 50) and
+  less (infix "\<sqsubset>" 50)
 
 end
 
diff -r 07f9732804ad -r 72d81e789106 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sun Feb 26 20:08:12 2012 +0100
+++ b/src/HOL/Orderings.thy	Sun Feb 26 20:10:14 2012 +0100
@@ -1426,8 +1426,4 @@
 lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
 lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
 
-no_notation
-  top ("\<top>") and
-  bot ("\<bottom>")
-
 end
diff -r 07f9732804ad -r 72d81e789106 src/HOL/Plain.thy
--- a/src/HOL/Plain.thy	Sun Feb 26 20:08:12 2012 +0100
+++ b/src/HOL/Plain.thy	Sun Feb 26 20:10:14 2012 +0100
@@ -9,4 +9,18 @@
   include @{text Hilbert_Choice}.
 *}
 
+no_notation
+  bot ("\<bottom>") and
+  top ("\<top>") and
+  inf (infixl "\<sqinter>" 70) and
+  sup (infixl "\<squnion>" 65) and
+  Inf ("\<Sqinter>_" [900] 900) and
+  Sup ("\<Squnion>_" [900] 900)
+
+no_syntax (xsymbols)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+
 end
diff -r 07f9732804ad -r 72d81e789106 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sun Feb 26 20:08:12 2012 +0100
+++ b/src/HOL/Relation.thy	Sun Feb 26 20:10:14 2012 +0100
@@ -939,19 +939,5 @@
   obtains "r x z"
   using assms by (auto dest: transD simp add: transp_def)
 
-no_notation
-  bot ("\<bottom>") and
-  top ("\<top>") and
-  inf (infixl "\<sqinter>" 70) and
-  sup (infixl "\<squnion>" 65) and
-  Inf ("\<Sqinter>_" [900] 900) and
-  Sup ("\<Squnion>_" [900] 900)
-
-no_syntax (xsymbols)
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
 end