src/HOL/Algebra/abstract/Ring2.thy
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