src/HOL/Library/FinFun_Syntax.thy
changeset 48041 d60f6b41bf2d
child 51542 738598beeb26
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/FinFun_Syntax.thy	Wed May 30 16:05:06 2012 +0200
     1.3 @@ -0,0 +1,25 @@
     1.4 +(* Author: Andreas Lochbihler, KIT *)
     1.5 +
     1.6 +header {* Pretty syntax for almost everywhere constant functions *}
     1.7 +
     1.8 +theory FinFun_Syntax imports FinFun begin
     1.9 +
    1.10 +type_notation
    1.11 +  finfun ("(_ =>f /_)" [22, 21] 21)
    1.12 +
    1.13 +type_notation (xsymbols)
    1.14 +  finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
    1.15 +
    1.16 +notation
    1.17 +  finfun_const ("K$/ _" [0] 1) and
    1.18 +  finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
    1.19 +  finfun_apply (infixl "$" 999) and
    1.20 +  finfun_comp (infixr "o$" 55) and
    1.21 +  finfun_comp2 (infixr "$o" 55) and
    1.22 +  finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
    1.23 +
    1.24 +notation (xsymbols) 
    1.25 +  finfun_comp (infixr "\<circ>$" 55) and
    1.26 +  finfun_comp2 (infixr "$\<circ>" 55)
    1.27 +
    1.28 +end
    1.29 \ No newline at end of file