src/HOL/Library/Lattice_Syntax.thy
author haftmann
Wed Apr 22 19:09:21 2009 +0200 (2009-04-22)
changeset 30960 fec1a04b7220
parent 30375 ad2a9dc516ed
child 32139 e271a64f03ff
permissions -rw-r--r--
power operation defined generic
     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 (*>*)