Robert Soeldner (Sep 01 2021 at 20:07): Robert Soeldner (Sep 01 2021 at 20:07):Is there any difference in writing rule_tac x = "" in exI or exI[where x = ""] ?
Wenda Li (Sep 02 2021 at 06:35):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.
Robert Soeldner (Sep 02 2021 at 17:31):thank you :)
Notification Bot (Sep 02 2021 at 17:31):Robert Soeldner has marked this topic as resolved.
Mathias Fleury (Sep 06 2021 at 05:14):There is a key difference: rule_tac x = x in exI can refer to a bound variable (like x in !!x. P x), while the where cannot.
Last updated: Nov 13 2025 at 08:29 UTC