User Tools

Site Tools



This shows you the differences between two versions of the page.

Link to this comparison view

reference:thin_tac [2014/07/29 10:05] (current) created
Line 1: Line 1:
 +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.
 +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