--- a/src/HOL/Library/FinFun.thy Wed May 30 10:04:05 2012 +0200
+++ b/src/HOL/Library/FinFun.thy Wed May 30 16:05:06 2012 +0200
@@ -1443,4 +1443,24 @@
(if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
by(simp add: finfun_to_list_update)
+text {* Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again *}
+
+no_type_notation
+ finfun ("(_ =>f /_)" [22, 21] 21)
+
+no_type_notation (xsymbols)
+ finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
+
+no_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)
+
+no_notation (xsymbols)
+ finfun_comp (infixr "\<circ>$" 55) and
+ finfun_comp2 (infixr "$\<circ>" 55)
+
end