author | Andreas Lochbihler |
Wed, 30 May 2012 16:05:06 +0200 | |
changeset 49056 | d60f6b41bf2d |
child 52679 | 738598beeb26 |
permissions | -rw-r--r-- |
Andreas@49056 | 1 |
(* Author: Andreas Lochbihler, KIT *) |
Andreas@49056 | 2 |
|
Andreas@49056 | 3 |
header {* Pretty syntax for almost everywhere constant functions *} |
Andreas@49056 | 4 |
|
Andreas@49056 | 5 |
theory FinFun_Syntax imports FinFun begin |
Andreas@49056 | 6 |
|
Andreas@49056 | 7 |
type_notation |
Andreas@49056 | 8 |
finfun ("(_ =>f /_)" [22, 21] 21) |
Andreas@49056 | 9 |
|
Andreas@49056 | 10 |
type_notation (xsymbols) |
Andreas@49056 | 11 |
finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21) |
Andreas@49056 | 12 |
|
Andreas@49056 | 13 |
notation |
Andreas@49056 | 14 |
finfun_const ("K$/ _" [0] 1) and |
Andreas@49056 | 15 |
finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and |
Andreas@49056 | 16 |
finfun_apply (infixl "$" 999) and |
Andreas@49056 | 17 |
finfun_comp (infixr "o$" 55) and |
Andreas@49056 | 18 |
finfun_comp2 (infixr "$o" 55) and |
Andreas@49056 | 19 |
finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000) |
Andreas@49056 | 20 |
|
Andreas@49056 | 21 |
notation (xsymbols) |
Andreas@49056 | 22 |
finfun_comp (infixr "\<circ>$" 55) and |
Andreas@49056 | 23 |
finfun_comp2 (infixr "$\<circ>" 55) |
Andreas@49056 | 24 |
|
Andreas@49056 | 25 |
end |