# HG changeset patch # User wenzelm # Date 1394803773 -3600 # Node ID 8bb21318e10b184440cf8fe0266298c29b0780d7 # Parent c06202417c4a207f36609b0a22c66a1ce38f32f7 tuned -- command 'text' was localized some years ago; diff -r c06202417c4a -r 8bb21318e10b src/HOL/Algebra/FiniteProduct.thy --- a/src/HOL/Algebra/FiniteProduct.thy Fri Mar 14 12:23:59 2014 +0100 +++ b/src/HOL/Algebra/FiniteProduct.thy Fri Mar 14 14:29:33 2014 +0100 @@ -456,7 +456,7 @@ text {*Usually, if this rule causes a failed congruence proof error, the reason is that the premise @{text "g \ B -> carrier G"} cannot be shown. Adding @{thm [source] Pi_def} to the simpset is often useful. - For this reason, @{thm [source] comm_monoid.finprod_cong} + For this reason, @{thm [source] finprod_cong} is not added to the simpset by default. *}