author | haftmann |
Sat, 19 Dec 2015 17:03:17 +0100 | |
changeset 61891 | 76189756ff65 |
parent 60500 | 903bb1495239 |
child 61955 | e96292f32c3c |
permissions | -rw-r--r-- |
30330 | 1 |
(* Author: Florian Haftmann, TU Muenchen *) |
2 |
||
60500 | 3 |
section \<open>Pretty syntax for lattice operations\<close> |
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 |