src/HOL/Library/Euclidean_Space.thy
changeset 30510 4120fc59dd85
parent 30489 5d7d0add1741
child 30549 d2d7874648bd
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -134,7 +134,7 @@
     1.4     (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)
     1.5     THEN' asm_full_simp_tac (ss2 addsimps ths)
     1.6   in
     1.7 -  Method.thms_args (Method.SIMPLE_METHOD' o vector_arith_tac)
     1.8 +  Method.thms_args (SIMPLE_METHOD' o vector_arith_tac)
     1.9  end
    1.10  *} "Lifts trivial vector statements to real arith statements"
    1.11  
    1.12 @@ -948,7 +948,7 @@
    1.13  
    1.14  use "normarith.ML"
    1.15  
    1.16 -method_setup norm = {* Method.ctxt_args (Method.SIMPLE_METHOD' o NormArith.norm_arith_tac)
    1.17 +method_setup norm = {* Method.ctxt_args (SIMPLE_METHOD' o NormArith.norm_arith_tac)
    1.18  *} "Proves simple linear statements about vector norms"
    1.19  
    1.20