# HG changeset patch
# User wenzelm
# Date 1194732232 -3600
# Node ID 72cfe89f7b218d731cd3603b6e008ed71decc9d5
# Parent  c100bf5bd6b8a9e5bb7f07a80db081ad8490ca94
tuned specifications of 'notation';

diff -r c100bf5bd6b8 -r 72cfe89f7b21 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sat Nov 10 18:36:10 2007 +0100
+++ b/src/HOL/Lattices.thy	Sat Nov 10 23:03:52 2007 +0100
@@ -12,9 +12,8 @@
 subsection{* Lattices *}
 
 notation
-  less_eq (infix "\<sqsubseteq>" 50)
-and
-  less    (infix "\<sqsubset>" 50)
+  less_eq  (infix "\<sqsubseteq>" 50) and
+  less  (infix "\<sqsubset>" 50)
 
 class lower_semilattice = order +
   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
@@ -30,6 +29,7 @@
 
 class lattice = lower_semilattice + upper_semilattice
 
+
 subsubsection{* Intro and elim rules*}
 
 context lower_semilattice
@@ -398,13 +398,11 @@
   by (simp add: Sup_insert_simp)
 
 definition
-  top :: 'a
-where
+  top :: 'a where
   "top = \<Sqinter>{}"
 
 definition
-  bot :: 'a
-where
+  bot :: 'a where
   "bot = \<Squnion>{}"
 
 lemma top_greatest [simp]: "x \<le> top"
@@ -586,16 +584,11 @@
 lemmas sup_aci = sup_ACI
 
 no_notation
-  less_eq (infix "\<sqsubseteq>" 50)
-and
-  less    (infix "\<sqsubset>" 50)
-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) and
+  inf  (infixl "\<sqinter>" 70) and
+  sup  (infixl "\<squnion>" 65) and
+  Inf  ("\<Sqinter>_" [900] 900) and
+  Sup  ("\<Squnion>_" [900] 900)
 
 end
diff -r c100bf5bd6b8 -r 72cfe89f7b21 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Nov 10 18:36:10 2007 +0100
+++ b/src/HOL/Nat.thy	Sat Nov 10 23:03:52 2007 +0100
@@ -1444,15 +1444,14 @@
 begin
 
 definition
-  Nats  :: "'a set"
-where
+  Nats  :: "'a set" where
   "Nats = range of_nat"
 
-end
-
 notation (xsymbols)
   Nats  ("\<nat>")
 
+end
+
 context semiring_1
 begin
 
diff -r c100bf5bd6b8 -r 72cfe89f7b21 src/HOL/Subst/Subst.thy
--- a/src/HOL/Subst/Subst.thy	Sat Nov 10 18:36:10 2007 +0100
+++ b/src/HOL/Subst/Subst.thy	Sat Nov 10 23:03:52 2007 +0100
@@ -22,14 +22,14 @@
 definition
   subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool"  (infixr "=$=" 52) where
   "r =$= s \<longleftrightarrow> (\<forall>t. t \<lhd> r = t \<lhd> s)"
-notation
+notation (xsymbols)
   subst_eq  (infixr "\<doteq>" 52)
 
 definition
   comp :: "[('a*('a uterm)) list, ('a*('a uterm)) list] => ('a*('a uterm)) list"
     (infixl "<>" 56) where
   "al <> bl = alist_rec al bl (%x y xs g. (x,y \<lhd> bl)#g)"
-notation
+notation (xsymbols)
   comp  (infixl "\<lozenge>" 56)
 
 definition
diff -r c100bf5bd6b8 -r 72cfe89f7b21 src/HOL/Word/BitSyntax.thy
--- a/src/HOL/Word/BitSyntax.thy	Sat Nov 10 18:36:10 2007 +0100
+++ b/src/HOL/Word/BitSyntax.thy	Sat Nov 10 23:03:52 2007 +0100
@@ -25,15 +25,9 @@
 *}
 
 notation
-  bitNOT  ("NOT _" [70] 71)
-
-notation
-  bitAND  (infixr "AND" 64)
-
-notation
-  bitOR   (infixr "OR"  59)
-
-notation
+  bitNOT  ("NOT _" [70] 71) and
+  bitAND  (infixr "AND" 64) and
+  bitOR   (infixr "OR"  59) and
   bitXOR  (infixr "XOR" 59)
 
 text {*