| author | blanchet |
| Fri, 21 Dec 2012 14:35:29 +0100 | |
| changeset 50610 | d9c4fbbb0c11 |
| parent 48041 | d60f6b41bf2d |
| child 51542 | 738598beeb26 |
| 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 |
|
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
3 |
header {* Pretty syntax for almost everywhere constant functions *}
|
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
4 |
|
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
5 |
theory FinFun_Syntax imports FinFun begin |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
6 |
|
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
7 |
type_notation |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
8 |
finfun ("(_ =>f /_)" [22, 21] 21)
|
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
9 |
|
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
10 |
type_notation (xsymbols) |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
11 |
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
|
12 |
|
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
13 |
notation |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
14 |
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
|
15 |
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
|
16 |
finfun_apply (infixl "$" 999) and |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
17 |
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
|
18 |
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
|
19 |
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
|
20 |
|
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
21 |
notation (xsymbols) |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
22 |
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
|
23 |
finfun_comp2 (infixr "$\<circ>" 55) |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
24 |
|
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
diff
changeset
|
25 |
end |