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