I’ve been using it a bit and it’s pretty useful! Thanks Larry > 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 [1]. 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev