equal
deleted
inserted
replaced
224 IF_UNSOLVED (*simp_tac may have finished it off!*) |
224 IF_UNSOLVED (*simp_tac may have finished it off!*) |
225 ((*simplify assumptions*) |
225 ((*simplify assumptions*) |
226 (*some risk of excessive simplification here -- might have |
226 (*some risk of excessive simplification here -- might have |
227 to identify the bare minimum set of rewrites*) |
227 to identify the bare minimum set of rewrites*) |
228 full_simp_tac |
228 full_simp_tac |
229 (mut_ss addsimps (conj_simps @ imp_simps @ quant_simps)) 1 |
229 (mut_ss addsimps conj_simps @ imp_simps @ quant_simps) 1 |
230 THEN |
230 THEN |
231 (*unpackage and use "prem" in the corresponding place*) |
231 (*unpackage and use "prem" in the corresponding place*) |
232 REPEAT (rtac impI 1) THEN |
232 REPEAT (rtac impI 1) THEN |
233 rtac (rewrite_rule all_defs prem) 1 THEN |
233 rtac (rewrite_rule all_defs prem) 1 THEN |
234 (*prem must not be REPEATed below: could loop!*) |
234 (*prem must not be REPEATed below: could loop!*) |