| changeset 30510 | 4120fc59dd85 |
| parent 29269 | 5c25a2012975 |
| child 30515 | bca05b17b618 |
--- a/src/HOL/Algebra/ringsimp.ML Fri Mar 13 19:53:09 2009 +0100 +++ b/src/HOL/Algebra/ringsimp.ML Fri Mar 13 19:58:26 2009 +0100 @@ -72,7 +72,7 @@ (** Setup **) val setup = - Method.add_methods [("algebra", Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac), + Method.add_methods [("algebra", Method.ctxt_args (SIMPLE_METHOD' o algebra_tac), "normalisation of algebraic structure")] #> Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];