equal
deleted
inserted
replaced
1 (* Author: Florian Haftmann, TU Muenchen *) |
1 (* Author: Florian Haftmann, TU Muenchen *) |
2 |
2 |
3 header {* Pretty syntax for lattice operations *} |
3 header {* Pretty syntax for lattice operations *} |
4 |
4 |
5 (*<*) |
|
6 theory Lattice_Syntax |
5 theory Lattice_Syntax |
7 imports Complete_Lattice |
6 imports Complete_Lattice |
8 begin |
7 begin |
9 |
8 |
10 notation |
9 notation |
14 sup (infixl "\<squnion>" 65) and |
13 sup (infixl "\<squnion>" 65) and |
15 Inf ("\<Sqinter>_" [900] 900) and |
14 Inf ("\<Sqinter>_" [900] 900) and |
16 Sup ("\<Squnion>_" [900] 900) |
15 Sup ("\<Squnion>_" [900] 900) |
17 |
16 |
18 end |
17 end |
19 (*>*) |
|