equal
deleted
inserted
replaced
2 |
2 |
3 header {* Pretty syntax for lattice operations *} |
3 header {* Pretty syntax for lattice operations *} |
4 |
4 |
5 (*<*) |
5 (*<*) |
6 theory Lattice_Syntax |
6 theory Lattice_Syntax |
7 imports Set |
7 imports Complete_Lattice |
8 begin |
8 begin |
9 |
9 |
10 notation |
10 notation |
|
11 top ("\<top>") and |
|
12 bot ("\<bottom>") and |
11 inf (infixl "\<sqinter>" 70) and |
13 inf (infixl "\<sqinter>" 70) and |
12 sup (infixl "\<squnion>" 65) and |
14 sup (infixl "\<squnion>" 65) and |
13 Inf ("\<Sqinter>_" [900] 900) and |
15 Inf ("\<Sqinter>_" [900] 900) and |
14 Sup ("\<Squnion>_" [900] 900) and |
16 Sup ("\<Squnion>_" [900] 900) |
15 top ("\<top>") and |
|
16 bot ("\<bottom>") |
|
17 |
17 |
18 end |
18 end |
19 (*>*) |
19 (*>*) |