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.
Last updated: Jul 15 2022 at 23:21 UTC