author | haftmann |
Fri, 06 Mar 2009 20:30:19 +0100 | |
changeset 30330 | 8291bc63d7c9 |
parent 30329 | 97ce36d801b6 |
child 30331 | 32ccef17d408 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Lattice_Syntax.thy Fri Mar 06 20:30:19 2009 +0100 @@ -0,0 +1,15 @@ +(* 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) + +end \ No newline at end of file