Re: [isabelle] Quick question about rule+
Steve W wrote:
> I'm wondering what apply rule+ does. I can't seem to find any mention of
> rule+ in the reference manual. Could someone please give some pointers?
rule tries to apply a rule that has an "intro?" attribute.
()+ is a tactic that repeats its argument tactic until it fails, at
cf §6.3.1 and §6.3.3 of Isabelle/Isar Reference manual.
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and