--- a/src/HOL/ex/FinFunPred.thy Wed May 30 09:46:58 2012 +0200
+++ b/src/HOL/ex/FinFunPred.thy Wed May 30 09:54:53 2012 +0200
@@ -20,7 +20,7 @@
instance ..
lemma le_finfun_code [code]:
- "f \<le> g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>$ (f, g)\<^sup>f)"
+ "f \<le> g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>$ ($f, g$))"
by(simp add: le_finfun_def finfun_All_All o_def)
end
@@ -48,7 +48,7 @@
by(auto simp add: top_finfun_def)
instantiation "finfun" :: (type, inf) inf begin
-definition [code]: "inf f g = (\<lambda>(x, y). inf x y) \<circ>$ (f, g)\<^sup>f"
+definition [code]: "inf f g = (\<lambda>(x, y). inf x y) \<circ>$ ($f, g$)"
instance ..
end
@@ -56,7 +56,7 @@
by(auto simp add: inf_finfun_def o_def inf_fun_def)
instantiation "finfun" :: (type, sup) sup begin
-definition [code]: "sup f g = (\<lambda>(x, y). sup x y) \<circ>$ (f, g)\<^sup>f"
+definition [code]: "sup f g = (\<lambda>(x, y). sup x y) \<circ>$ ($f, g$)"
instance ..
end
@@ -78,7 +78,7 @@
by(intro_classes)(simp add: sup_finfun_def inf_finfun_def expand_finfun_eq o_def sup_inf_distrib1)
instantiation "finfun" :: (type, minus) minus begin
-definition "f - g = split (op -) \<circ>$ (f, g)\<^sup>f"
+definition "f - g = split (op -) \<circ>$ ($f, g$)"
instance ..
end