User Tools
reference:thin_tac
Differences
This shows you the differences between two versions of the page.
| — |
reference:thin_tac [2014/07/29 10:05] (current) 131.246.38.230 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. | ||
| + | |||
| + | 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
Page Tools
