--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sat Jul 18 20:54:56 2015 +0200
@@ -127,8 +127,8 @@
@{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 Cartesian_Euclidean_Space.setsum_cong_aux} i
- ORELSE rtac @{thm setsum.neutral} i
+ THEN' (fn i => resolve_tac ctxt @{thms Cartesian_Euclidean_Space.setsum_cong_aux} i
+ ORELSE resolve_tac ctxt @{thms setsum.neutral} 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 (put_simpset ss2 ctxt addsimps ths)