30330
|
1 |
(* Author: Florian Haftmann, TU Muenchen *)
|
|
2 |
|
|
3 |
header {* Pretty syntax for lattice operations *}
|
|
4 |
|
|
5 |
theory Lattice_Syntax
|
32139
|
6 |
imports Complete_Lattice
|
30330
|
7 |
begin
|
|
8 |
|
|
9 |
notation
|
32139
|
10 |
top ("\<top>") and
|
|
11 |
bot ("\<bottom>") 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)
|
|
18 |
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
|
|
19 |
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
|
|
20 |
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
|
|
21 |
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
|
|
22 |
|
30331
|
23 |
end
|