author | wenzelm |
Sun, 02 Nov 2014 17:20:45 +0100 | |
changeset 58881 | b9556a055632 |
parent 44860 | 56101fa00193 |
child 60500 | 903bb1495239 |
permissions | -rw-r--r-- |
30330 | 1 |
(* Author: Florian Haftmann, TU Muenchen *) |
2 |
||
58881 | 3 |
section {* Pretty syntax for lattice operations *} |
30330 | 4 |
|
5 |
theory Lattice_Syntax |
|
44860
56101fa00193
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
haftmann
parents:
41082
diff
changeset
|
6 |
imports Complete_Lattices |
30330 | 7 |
begin |
8 |
||
9 |
notation |
|
41082 | 10 |
bot ("\<bottom>") and |
32139 | 11 |
top ("\<top>") and |
30330 | 12 |
inf (infixl "\<sqinter>" 70) and |
13 |
sup (infixl "\<squnion>" 65) and |
|
14 |
Inf ("\<Sqinter>_" [900] 900) and |
|
32139 | 15 |
Sup ("\<Squnion>_" [900] 900) |
30330 | 16 |
|
41080 | 17 |
syntax (xsymbols) |
41082 | 18 |
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
19 |
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
|
41080 | 20 |
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |
21 |
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
|
22 |
||
30331 | 23 |
end |