src/HOL/Library/FinFun_Syntax.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/FinFun_Syntax.thy	Wed May 30 16:05:06 2012 +0200
@@ -0,0 +1,25 @@
+(* Author: Andreas Lochbihler, KIT *)
+
+header {* Pretty syntax for almost everywhere constant functions *}
+
+theory FinFun_Syntax imports FinFun begin
+
+type_notation
+  finfun ("(_ =>f /_)" [22, 21] 21)
+
+type_notation (xsymbols)
+  finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
+
+notation
+  finfun_const ("K$/ _" [0] 1) and
+  finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
+  finfun_apply (infixl "$" 999) and
+  finfun_comp (infixr "o$" 55) and
+  finfun_comp2 (infixr "$o" 55) and
+  finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
+
+notation (xsymbols) 
+  finfun_comp (infixr "\<circ>$" 55) and
+  finfun_comp2 (infixr "$\<circ>" 55)
+
+end
\ No newline at end of file