src/HOL/Number_Theory/MiscAlgebra.thy
changeset 57514 bdc2c6b40bf2
parent 55322 3bf50e3cd727
child 60526 fad653acf58f
     1.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4    apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
     1.5    apply auto
     1.6  (* auto should get this. I suppose we need "comm_monoid_simprules"
     1.7 -   for mult_ac rewriting. *)
     1.8 +   for ac_simps rewriting. *)
     1.9    apply (subst m_assoc [symmetric])
    1.10    apply auto
    1.11    done