| author | haftmann | 
| Wed, 13 Jan 2010 08:56:25 +0100 | |
| changeset 34889 | dcaf6ec84e28 | 
| parent 32139 | e271a64f03ff | 
| child 35787 | afdf1c4958b2 | 
| permissions | -rw-r--r-- | 
(* Author: Florian Haftmann, TU Muenchen *) header {* Pretty syntax for lattice operations *} (*<*) theory Lattice_Syntax imports Complete_Lattice begin notation top ("\<top>") and bot ("\<bottom>") and inf (infixl "\<sqinter>" 70) and sup (infixl "\<squnion>" 65) and Inf ("\<Sqinter>_" [900] 900) and Sup ("\<Squnion>_" [900] 900) end (*>*)