Re: [isabelle] Quick question about rule+

Steve W wrote:
> Hi,
> 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?
> Thanks
> Steve
rule tries to apply a rule that has an "intro?" attribute.
()+ is a tactic that repeats its argument tactic until it fails, at
least once.

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 MHonArc.