src/HOL/Library/Euclidean_Space.thy
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
child 30582 638b088bb840
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Mon Mar 16 17:51:24 2009 +0100
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon Mar 16 18:24:30 2009 +0100
     1.3 @@ -134,8 +134,8 @@
     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 (SIMPLE_METHOD' o vector_arith_tac)
     1.8 -end
     1.9 +  Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths)))
    1.10 + end
    1.11  *} "Lifts trivial vector statements to real arith statements"
    1.12  
    1.13  lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def)
    1.14 @@ -948,7 +948,7 @@
    1.15  
    1.16  use "normarith.ML"
    1.17  
    1.18 -method_setup norm = {* Method.ctxt_args (SIMPLE_METHOD' o NormArith.norm_arith_tac)
    1.19 +method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
    1.20  *} "Proves simple linear statements about vector norms"
    1.21  
    1.22