equal
deleted
inserted
replaced
427 | _ => [th]) |
427 | _ => [th]) |
428 in atoms end; |
428 in atoms end; |
429 |
429 |
430 fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all); |
430 fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all); |
431 |
431 |
432 fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems), |
432 fun unsafe_solver prems = FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), |
433 atac, etac FalseE]; |
433 atac , etac FalseE ]; |
434 (*No premature instantiation of variables during simplification*) |
434 (*No premature instantiation of variables during simplification*) |
435 fun safe_solver prems = FIRST'[match_tac (reflexive_thm::TrueI::prems), |
435 fun safe_solver prems = FIRST'[ match_tac(reflexive_thm::TrueI::refl::prems), |
436 eq_assume_tac, ematch_tac [FalseE]]; |
436 eq_assume_tac, ematch_tac [FalseE]]; |
437 |
437 |
438 val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac |
438 val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac |
439 setSSolver safe_solver |
439 setSSolver safe_solver |
440 setSolver unsafe_solver |
440 setSolver unsafe_solver |