Is there any difference in writing
rule_tac x = "" in exI or
exI[where x = ""] ?
Not much difference to me, but I believe people may slightly favour the latter as the former is sometimes considered 'improper' proof methods.
"The following improper proof methods emulate traditional tactics. These admit direct access to the goal state, which is normally considered harmful!" ---isar-ref, p169.
thank you :)
Robert Soeldner has marked this topic as resolved.
There is a key difference:
rule_tac x = x in exI can refer to a bound variable (like
!!x. P x), while the where cannot.
Last updated: Aug 13 2022 at 05:18 UTC