Re: [isabelle-dev] The coming release of Isabelle2017

I currently supervise a student who's investigating proof refactoring. One possible outcome of this would be a tool that also does what you suggested. It's a little too early to tell, though. Cheers Lars On 8 July 2017 23:28:42 CEST, Lawrence Paulson wrote: >No, that’s

Re: [isabelle-dev] The coming release of Isabelle2017

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). Fabian [1]