Stream: Beginner Questions

Topic: rule_tac vs [where ..]

view this post on Zulip Robert Soeldner (Sep 01 2021 at 20:07):

Is there any difference in writing rule_tac x = "" in exI or exI[where x = ""] ?

view this post on Zulip 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.

Last updated: Jul 15 2022 at 23:21 UTC