Re: [isabelle] Quick question about rule+



On Wed, 2 Sep 2009, 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?

The "+" Operator repeats any proof method, not just "rule". See 6.3.1 "Proof method expressions" in the isar-ref manual.


	Makarius






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