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,
  Peter





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.