changeset 30515 | 4120fc59dd85 |
parent 29669 | 2a580d9af918 |
child 30549 | d2d7874648bd |
1.1 --- a/src/HOL/Algebra/abstract/Ring2.thy Fri Mar 13 19:53:09 2009 +0100 1.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy Fri Mar 13 19:58:26 2009 +0100 1.3 @@ -222,7 +222,7 @@ 1.4 *} (* Note: r_one is not necessary in ring_ss *) 1.5 1.6 method_setup ring = 1.7 - {* Method.no_args (Method.SIMPLE_METHOD' (full_simp_tac ring_ss)) *} 1.8 + {* Method.no_args (SIMPLE_METHOD' (full_simp_tac ring_ss)) *} 1.9 {* computes distributive normal form in rings *} 1.10 1.11