| author | wenzelm |
| Mon Dec 28 17:43:30 2015 +0100 (2015-12-28) | |
| changeset 61952 | 546958347e05 |
| parent 60500 | 903bb1495239 |
| child 61955 | e96292f32c3c |
| permissions | -rw-r--r-- |
| haftmann@30330 | 1 |
(* Author: Florian Haftmann, TU Muenchen *) |
| haftmann@30330 | 2 |
|
| wenzelm@60500 | 3 |
section \<open>Pretty syntax for lattice operations\<close> |
| haftmann@30330 | 4 |
|
| haftmann@30330 | 5 |
theory Lattice_Syntax |
| haftmann@44860 | 6 |
imports Complete_Lattices |
| haftmann@30330 | 7 |
begin |
| haftmann@30330 | 8 |
|
| haftmann@30330 | 9 |
notation |
| haftmann@41082 | 10 |
bot ("\<bottom>") and
|
| haftmann@32139 | 11 |
top ("\<top>") and
|
| haftmann@30330 | 12 |
inf (infixl "\<sqinter>" 70) and |
| haftmann@30330 | 13 |
sup (infixl "\<squnion>" 65) and |
| haftmann@30330 | 14 |
Inf ("\<Sqinter>_" [900] 900) and
|
| haftmann@32139 | 15 |
Sup ("\<Squnion>_" [900] 900)
|
| haftmann@30330 | 16 |
|
| haftmann@41080 | 17 |
syntax (xsymbols) |
| haftmann@41082 | 18 |
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
|
| haftmann@41082 | 19 |
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
|
| haftmann@41080 | 20 |
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
|
| haftmann@41080 | 21 |
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
|
| haftmann@41080 | 22 |
|
| haftmann@30331 | 23 |
end |