src/HOL/Library/Lattice_Syntax.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 32139 e271a64f03ff
child 35787 afdf1c4958b2
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Pretty syntax for lattice operations *}
     4 
     5 (*<*)
     6 theory Lattice_Syntax
     7 imports Complete_Lattice
     8 begin
     9 
    10 notation
    11   top ("\<top>") and
    12   bot ("\<bottom>") and
    13   inf  (infixl "\<sqinter>" 70) and
    14   sup  (infixl "\<squnion>" 65) and
    15   Inf  ("\<Sqinter>_" [900] 900) and
    16   Sup  ("\<Squnion>_" [900] 900)
    17 
    18 end
    19 (*>*)