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 (*<*) |
5 theory Lattice_Syntax |
6 theory Lattice_Syntax |
6 imports Set |
7 imports Set |
7 begin |
8 begin |
8 |
9 |
9 notation |
10 notation |
11 sup (infixl "\<squnion>" 65) and |
12 sup (infixl "\<squnion>" 65) and |
12 Inf ("\<Sqinter>_" [900] 900) and |
13 Inf ("\<Sqinter>_" [900] 900) and |
13 Sup ("\<Squnion>_" [900] 900) |
14 Sup ("\<Squnion>_" [900] 900) |
14 |
15 |
15 end |
16 end |
|
17 (*>*) |