I’ve been using it a bit and it’s pretty useful! Thanks
> On 9 Jul 2017, at 17:16, Fabian Immler <imm...@in.tum.de> wrote:
> A while ago, Florian Haftmann sent a command that does something like this to
> the mailing list . I attach a version that works with current
> Isabelle2016-1 (not sure if I got all the modifications right, but it seems
> to work at least on the example in the .thy file).
isabelle-dev mailing list