author | nipkow |
Sat, 26 Aug 2017 16:47:25 +0200 | |
changeset 66515 | 85c505c98332 |
parent 66453 | cc19f7ca2ed6 |
child 68660 | 4ce18f389f53 |
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 |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
61955
diff
changeset
|
6 |
imports HOL.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 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
60500
diff
changeset
|
17 |
syntax |
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 |