author | wenzelm |
Mon, 06 Jul 2015 22:06:02 +0200 | |
changeset 60678 | 17ba2df56dee |
parent 60500 | 903bb1495239 |
child 61384 | 9f5145281888 |
permissions | -rw-r--r-- |
48041
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
1 |
(* Author: Andreas Lochbihler, KIT *) |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
2 |
|
60500 | 3 |
section \<open>Pretty syntax for almost everywhere constant functions\<close> |
48041
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
4 |
|
51542 | 5 |
theory FinFun_Syntax |
6 |
imports FinFun |
|
7 |
begin |
|
48041
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
8 |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
9 |
type_notation |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
10 |
finfun ("(_ =>f /_)" [22, 21] 21) |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
11 |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
12 |
type_notation (xsymbols) |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
13 |
finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21) |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
14 |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
15 |
notation |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
16 |
finfun_const ("K$/ _" [0] 1) and |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
17 |
finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
18 |
finfun_apply (infixl "$" 999) and |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
19 |
finfun_comp (infixr "o$" 55) and |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
20 |
finfun_comp2 (infixr "$o" 55) and |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
21 |
finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000) |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
22 |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
23 |
notation (xsymbols) |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
24 |
finfun_comp (infixr "\<circ>$" 55) and |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
25 |
finfun_comp2 (infixr "$\<circ>" 55) |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
26 |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
27 |
end |