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.