src/HOL/Library/Function_Algebras.thy
changeset 60562 24af00b010cf
parent 60500 903bb1495239
child 60679 ade12ef2773c
--- a/src/HOL/Library/Function_Algebras.thy	Mon Jun 22 23:19:48 2015 +0200
+++ b/src/HOL/Library/Function_Algebras.thy	Tue Jun 23 16:55:28 2015 +0100
@@ -154,7 +154,8 @@
 
 instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
 
-instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
+instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel 
+  by default (auto simp add: times_fun_def algebra_simps)
 
 instance "fun" :: (type, semiring_char_0) semiring_char_0
 proof