tuned specifications of 'notation';
authorwenzelm
Sat Nov 10 23:03:52 2007 +0100 (2007-11-10)
changeset 2538272cfe89f7b21
parent 25381 c100bf5bd6b8
child 25383 2e766dd19e4f
tuned specifications of 'notation';
src/HOL/Lattices.thy
src/HOL/Nat.thy
src/HOL/Subst/Subst.thy
src/HOL/Word/BitSyntax.thy
     1.1 --- a/src/HOL/Lattices.thy	Sat Nov 10 18:36:10 2007 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Sat Nov 10 23:03:52 2007 +0100
     1.3 @@ -12,9 +12,8 @@
     1.4  subsection{* Lattices *}
     1.5  
     1.6  notation
     1.7 -  less_eq (infix "\<sqsubseteq>" 50)
     1.8 -and
     1.9 -  less    (infix "\<sqsubset>" 50)
    1.10 +  less_eq  (infix "\<sqsubseteq>" 50) and
    1.11 +  less  (infix "\<sqsubset>" 50)
    1.12  
    1.13  class lower_semilattice = order +
    1.14    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    1.15 @@ -30,6 +29,7 @@
    1.16  
    1.17  class lattice = lower_semilattice + upper_semilattice
    1.18  
    1.19 +
    1.20  subsubsection{* Intro and elim rules*}
    1.21  
    1.22  context lower_semilattice
    1.23 @@ -398,13 +398,11 @@
    1.24    by (simp add: Sup_insert_simp)
    1.25  
    1.26  definition
    1.27 -  top :: 'a
    1.28 -where
    1.29 +  top :: 'a where
    1.30    "top = \<Sqinter>{}"
    1.31  
    1.32  definition
    1.33 -  bot :: 'a
    1.34 -where
    1.35 +  bot :: 'a where
    1.36    "bot = \<Squnion>{}"
    1.37  
    1.38  lemma top_greatest [simp]: "x \<le> top"
    1.39 @@ -586,16 +584,11 @@
    1.40  lemmas sup_aci = sup_ACI
    1.41  
    1.42  no_notation
    1.43 -  less_eq (infix "\<sqsubseteq>" 50)
    1.44 -and
    1.45 -  less    (infix "\<sqsubset>" 50)
    1.46 -and
    1.47 -  inf     (infixl "\<sqinter>" 70)
    1.48 -and
    1.49 -  sup     (infixl "\<squnion>" 65)
    1.50 -and
    1.51 -  Inf     ("\<Sqinter>_" [900] 900)
    1.52 -and
    1.53 -  Sup     ("\<Squnion>_" [900] 900)
    1.54 +  less_eq  (infix "\<sqsubseteq>" 50) and
    1.55 +  less (infix "\<sqsubset>" 50) and
    1.56 +  inf  (infixl "\<sqinter>" 70) and
    1.57 +  sup  (infixl "\<squnion>" 65) and
    1.58 +  Inf  ("\<Sqinter>_" [900] 900) and
    1.59 +  Sup  ("\<Squnion>_" [900] 900)
    1.60  
    1.61  end
     2.1 --- a/src/HOL/Nat.thy	Sat Nov 10 18:36:10 2007 +0100
     2.2 +++ b/src/HOL/Nat.thy	Sat Nov 10 23:03:52 2007 +0100
     2.3 @@ -1444,15 +1444,14 @@
     2.4  begin
     2.5  
     2.6  definition
     2.7 -  Nats  :: "'a set"
     2.8 -where
     2.9 +  Nats  :: "'a set" where
    2.10    "Nats = range of_nat"
    2.11  
    2.12 -end
    2.13 -
    2.14  notation (xsymbols)
    2.15    Nats  ("\<nat>")
    2.16  
    2.17 +end
    2.18 +
    2.19  context semiring_1
    2.20  begin
    2.21  
     3.1 --- a/src/HOL/Subst/Subst.thy	Sat Nov 10 18:36:10 2007 +0100
     3.2 +++ b/src/HOL/Subst/Subst.thy	Sat Nov 10 23:03:52 2007 +0100
     3.3 @@ -22,14 +22,14 @@
     3.4  definition
     3.5    subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool"  (infixr "=$=" 52) where
     3.6    "r =$= s \<longleftrightarrow> (\<forall>t. t \<lhd> r = t \<lhd> s)"
     3.7 -notation
     3.8 +notation (xsymbols)
     3.9    subst_eq  (infixr "\<doteq>" 52)
    3.10  
    3.11  definition
    3.12    comp :: "[('a*('a uterm)) list, ('a*('a uterm)) list] => ('a*('a uterm)) list"
    3.13      (infixl "<>" 56) where
    3.14    "al <> bl = alist_rec al bl (%x y xs g. (x,y \<lhd> bl)#g)"
    3.15 -notation
    3.16 +notation (xsymbols)
    3.17    comp  (infixl "\<lozenge>" 56)
    3.18  
    3.19  definition
     4.1 --- a/src/HOL/Word/BitSyntax.thy	Sat Nov 10 18:36:10 2007 +0100
     4.2 +++ b/src/HOL/Word/BitSyntax.thy	Sat Nov 10 23:03:52 2007 +0100
     4.3 @@ -25,15 +25,9 @@
     4.4  *}
     4.5  
     4.6  notation
     4.7 -  bitNOT  ("NOT _" [70] 71)
     4.8 -
     4.9 -notation
    4.10 -  bitAND  (infixr "AND" 64)
    4.11 -
    4.12 -notation
    4.13 -  bitOR   (infixr "OR"  59)
    4.14 -
    4.15 -notation
    4.16 +  bitNOT  ("NOT _" [70] 71) and
    4.17 +  bitAND  (infixr "AND" 64) and
    4.18 +  bitOR   (infixr "OR"  59) and
    4.19    bitXOR  (infixr "XOR" 59)
    4.20  
    4.21  text {*