changeset 61169 | 4de9ff3ea29a |
parent 61032 | b57df8eecad6 |
child 61378 | 3e04c9ca001a |
--- a/src/HOL/Groups_Big.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Groups_Big.thy Sun Sep 13 22:56:52 2015 +0200 @@ -18,7 +18,7 @@ begin interpretation comp_fun_commute f - by default (simp add: fun_eq_iff left_commute) + by standard (simp add: fun_eq_iff left_commute) interpretation comp?: comp_fun_commute "f \<circ> g" by (fact comp_comp_fun_commute)