src/HOL/Lattices.thy
changeset 25382 72cfe89f7b21
parent 25206 9c84ec7217a9
child 25482 4ed49eccb1eb
     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