src/HOL/Library/Lattice_Syntax.thy
author huffman
Thu Jun 11 09:03:24 2009 -0700 (2009-06-11)
changeset 31563 ded2364d14d4
parent 30375 ad2a9dc516ed
child 32139 e271a64f03ff
permissions -rw-r--r--
cleaned up some proofs
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Pretty syntax for lattice operations *}
     4 
     5 (*<*)
     6 theory Lattice_Syntax
     7 imports Set
     8 begin
     9 
    10 notation
    11   inf  (infixl "\<sqinter>" 70) and
    12   sup  (infixl "\<squnion>" 65) and
    13   Inf  ("\<Sqinter>_" [900] 900) and
    14   Sup  ("\<Squnion>_" [900] 900) and
    15   top ("\<top>") and
    16   bot ("\<bottom>")
    17 
    18 end
    19 (*>*)