src/HOL/Library/Lattice_Syntax.thy
changeset 30375 ad2a9dc516ed
parent 30331 32ccef17d408
child 32139 e271a64f03ff
     1.1 --- a/src/HOL/Library/Lattice_Syntax.thy	Sun Mar 08 15:25:28 2009 +0100
     1.2 +++ b/src/HOL/Library/Lattice_Syntax.thy	Sun Mar 08 15:25:29 2009 +0100
     1.3 @@ -11,7 +11,9 @@
     1.4    inf  (infixl "\<sqinter>" 70) and
     1.5    sup  (infixl "\<squnion>" 65) and
     1.6    Inf  ("\<Sqinter>_" [900] 900) and
     1.7 -  Sup  ("\<Squnion>_" [900] 900)
     1.8 +  Sup  ("\<Squnion>_" [900] 900) and
     1.9 +  top ("\<top>") and
    1.10 +  bot ("\<bottom>")
    1.11  
    1.12  end
    1.13  (*>*)
    1.14 \ No newline at end of file