author | huffman |
Thu, 12 Mar 2009 08:57:03 -0700 | |
changeset 30488 | 5c4c3a9e9102 |
parent 30375 | ad2a9dc516ed |
child 32139 | e271a64f03ff |
permissions | -rw-r--r-- |
(* Author: Florian Haftmann, TU Muenchen *) header {* Pretty syntax for lattice operations *} (*<*) theory Lattice_Syntax imports Set begin notation inf (infixl "\<sqinter>" 70) and sup (infixl "\<squnion>" 65) and Inf ("\<Sqinter>_" [900] 900) and Sup ("\<Squnion>_" [900] 900) and top ("\<top>") and bot ("\<bottom>") end (*>*)