changeset 54745 | 46e441e61ff5 |
parent 54744 | 1e7f2d296e19 |
child 55096 | 916b2ac758f4 |
--- a/src/HOL/Groups_Big.thy Sun Dec 15 15:10:14 2013 +0100 +++ b/src/HOL/Groups_Big.thy Sun Dec 15 15:10:16 2013 +0100 @@ -20,8 +20,8 @@ interpretation comp_fun_commute f by default (simp add: fun_eq_iff left_commute) -interpretation comp_fun_commute "f \<circ> g" - by (rule comp_comp_fun_commute) +interpretation comp?: comp_fun_commute "f \<circ> g" + by (fact comp_comp_fun_commute) definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a" where