304 fun pair_upd1 f ((a,b),x) = (f(a,x), b); |
304 fun pair_upd1 f ((a,b),x) = (f(a,x), b); |
305 fun pair_upd2 f ((a,b),x) = (a, f(b,x)); |
305 fun pair_upd2 f ((a,b),x) = (a, f(b,x)); |
306 |
306 |
307 infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 |
307 infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 |
308 addsimps2 delsimps2 addcongs2 delcongs2; |
308 addsimps2 delsimps2 addcongs2 delcongs2; |
309 val op addSIs2 = pair_upd1 (op addSIs); |
309 fun op addSIs2 arg = pair_upd1 (op addSIs) arg; |
310 val op addSEs2 = pair_upd1 (op addSEs); |
310 fun op addSEs2 arg = pair_upd1 (op addSEs) arg; |
311 val op addSDs2 = pair_upd1 (op addSDs); |
311 fun op addSDs2 arg = pair_upd1 (op addSDs) arg; |
312 val op addIs2 = pair_upd1 (op addIs ); |
312 fun op addIs2 arg = pair_upd1 (op addIs ) arg; |
313 val op addEs2 = pair_upd1 (op addEs ); |
313 fun op addEs2 arg = pair_upd1 (op addEs ) arg; |
314 val op addDs2 = pair_upd1 (op addDs ); |
314 fun op addDs2 arg = pair_upd1 (op addDs ) arg; |
315 val op addsimps2 = pair_upd2 (op addsimps); |
315 fun op addsimps2 arg = pair_upd2 (op addsimps) arg; |
316 val op delsimps2 = pair_upd2 (op delsimps); |
316 fun op delsimps2 arg = pair_upd2 (op delsimps) arg; |
317 val op addcongs2 = pair_upd2 (op addcongs); |
317 fun op addcongs2 arg = pair_upd2 (op addcongs) arg; |
318 val op delcongs2 = pair_upd2 (op delcongs); |
318 fun op delcongs2 arg = pair_upd2 (op delcongs) arg; |
319 |
319 |
320 fun auto_tac (cs,ss) = let val cs' = cs addss ss in |
320 fun auto_tac (cs,ss) = let val cs' = cs addss ss in |
321 EVERY [ TRY (safe_tac cs'), |
321 EVERY [ TRY (safe_tac cs'), |
322 REPEAT (FIRSTGOAL (fast_tac cs')), |
322 REPEAT (FIRSTGOAL (fast_tac cs')), |
323 prune_params_tac] end; |
323 prune_params_tac] end; |