Use thin_tac to throw away assumptions that you don't need in order to prove your subgoal. Thin_tac needs a scheme for knowing, which assumption it should use. The first matching assumption will be deleted.

Examples:

lemma “⟦P t0;∀t. P t⟧ ⟹ P t0” apply (thin_tac “∀x. P x”) goal (1 subgoal): 1. P t0 ⟹ P t0

forget all assumptions: use a always matching scheme as often as possible apply (thin_tac ”?x”)+

reference/thin_tac.txt · Last modified: 2014/07/29 10:05 by 131.246.38.230
 
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki