This is an old revision of the document!
rule
is a proof method. It applies a rule if possible.
Assume we have a subgoal
and we want to use rule
with rule
Then, rule
does the following:
With rule_tac
, you can force schematic variables in the used rule to take specific values. The extended syntax is:
apply (rule_tac ident1="expr1" and ident2="expr1" and ... in rule)
This means that the variables ?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
.