equal
deleted
inserted
replaced
5 theory Lattice_Syntax |
5 theory Lattice_Syntax |
6 imports Complete_Lattice |
6 imports Complete_Lattice |
7 begin |
7 begin |
8 |
8 |
9 notation |
9 notation |
|
10 bot ("\<bottom>") and |
10 top ("\<top>") and |
11 top ("\<top>") and |
11 bot ("\<bottom>") and |
|
12 inf (infixl "\<sqinter>" 70) and |
12 inf (infixl "\<sqinter>" 70) and |
13 sup (infixl "\<squnion>" 65) and |
13 sup (infixl "\<squnion>" 65) and |
14 Inf ("\<Sqinter>_" [900] 900) and |
14 Inf ("\<Sqinter>_" [900] 900) and |
15 Sup ("\<Squnion>_" [900] 900) |
15 Sup ("\<Squnion>_" [900] 900) |
16 |
16 |
17 syntax (xsymbols) |
17 syntax (xsymbols) |
|
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) |
18 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |
20 "_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) |
21 "_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 |
22 |
23 end |
23 end |