User Tools
reference:rule_method
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
reference:rule_method [2011/06/22 11:59] 131.246.161.187 |
reference:rule_method [2011/06/22 12:19] 131.246.161.187 |
||
|---|---|---|---|
| Line 24: | Line 24: | ||
| apply (rule_tac ident1="expr1" and ident2="expr1" and ... in rule) | apply (rule_tac ident1="expr1" and ident2="expr1" and ... in rule) | ||
| This means that the variable ''?ident1'' is replaced by expression ''expr1'' and similarly for the others. Note that you have to leave out the question mark marking schematic variables. Find out which variables a rule uses with ''thm rule''. | This means that the variable ''?ident1'' is replaced by expression ''expr1'' and similarly for the others. Note that you have to leave out the question mark marking schematic variables. Find out which variables a rule uses with ''thm rule''. | ||
| + | |||
| + | === rule(k) === | ||
| + | Oftentimes, a rule application results in several subgoals that can directly be solved by ''[[assumption]]''; see [[#Example|above]] for an example. Instead of applying ''assumption'' by hand, you can apply ''rule(k)'' which forces Isabelle to apply ''assumption'' $k$ times after the rule application. | ||
| ==== Relatives ==== | ==== Relatives ==== | ||
reference/rule_method.txt ยท Last modified: 2011/06/22 12:27 by 131.246.161.187
Page Tools
