author | wenzelm |
Sat, 02 Aug 2014 19:29:02 +0200 | |
changeset 57843 | d8966c09025c |
parent 51542 | 738598beeb26 |
child 58881 | b9556a055632 |
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 |
|
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 |