equal
deleted
inserted
replaced
531 |
531 |
532 (*delete needless equality assumptions*) |
532 (*delete needless equality assumptions*) |
533 val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"} |
533 val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"} |
534 (fn _ => assume_tac 1); |
534 (fn _ => assume_tac 1); |
535 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE]; |
535 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE]; |
536 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls; |
536 val elim_tac = REPEAT o eresolve_tac elim_rls; |
537 |
537 |
538 fun simp_case_tac ctxt i = |
538 fun simp_case_tac ctxt i = |
539 EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i; |
539 EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i; |
540 |
540 |
541 in |
541 in |