src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy

 
 subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}
 
 method_setup vector = {*
 let
-  val ss1 = HOL_basic_ss addsimps [@{thm setsum_addf} RS sym,
-    @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib},
-    @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym]
-  val ss2 = @{simpset} addsimps
+  val ss1 =
+    simpset_of (put_simpset HOL_basic_ss @{context}
+      addsimps [@{thm setsum_addf} RS sym,
+      @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib},
+      @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym])
+  val ss2 =
+    simpset_of (@{context} addsimps
              [@{thm plus_vec_def}, @{thm times_vec_def},
               @{thm minus_vec_def}, @{thm uminus_vec_def},
               @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def},
               @{thm scaleR_vec_def},
-              @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}]
-  fun vector_arith_tac ths =
-    simp_tac ss1
+              @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}])
+  fun vector_arith_tac ctxt ths =
+    simp_tac (put_simpset ss1 ctxt)
     THEN' (fn i => rtac @{thm setsum_cong2} i
          ORELSE rtac @{thm setsum_0'} i
-         ORELSE simp_tac (HOL_basic_ss addsimps [@{thm vec_eq_iff}]) i)
+         ORELSE simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm vec_eq_iff}]) i)
     (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)
-    THEN' asm_full_simp_tac (ss2 addsimps ths)
+    THEN' asm_full_simp_tac (put_simpset ss2 ctxt addsimps ths)
 in
-  Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths)))
+  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (vector_arith_tac ctxt ths))
 end
 *} "lift trivial vector statements to real arith statements"
 
 lemma vec_0[simp]: "vec 0 = 0" by (vector zero_vec_def)
 lemma vec_1[simp]: "vec 1 = 1" by (vector one_vec_def)