equal
deleted
inserted
replaced
190 IF_UNSOLVED (*simp_tac may have finished it off!*) |
190 IF_UNSOLVED (*simp_tac may have finished it off!*) |
191 ((*simplify assumptions*) |
191 ((*simplify assumptions*) |
192 (*some risk of excessive simplification here -- might have |
192 (*some risk of excessive simplification here -- might have |
193 to identify the bare minimum set of rewrites*) |
193 to identify the bare minimum set of rewrites*) |
194 full_simp_tac |
194 full_simp_tac |
195 (mut_ss addsimps (conj_rews @ imp_rews @ quant_rews)) 1 THEN |
195 (mut_ss addsimps (conj_simps @ imp_simps @ quant_simps)) 1 |
|
196 THEN |
196 (*unpackage and use "prem" in the corresponding place*) |
197 (*unpackage and use "prem" in the corresponding place*) |
197 REPEAT (rtac impI 1) THEN |
198 REPEAT (rtac impI 1) THEN |
198 rtac (rewrite_rule all_defs prem) 1 THEN |
199 rtac (rewrite_rule all_defs prem) 1 THEN |
199 (*prem must not be REPEATed below: could loop!*) |
200 (*prem must not be REPEATed below: could loop!*) |
200 DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' |
201 DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' |