On Wed, 11 Apr 2012, Nils Jähnig wrote:
wow, this is uber-useful. especially apply auto  thank you, Peter. this is not in the tutorial, isn't it? i think it should.
Better see the isar-ref manual for all the details. If something is wrong or outdated there, do say so.