Re: [isabelle-dev] Explorer.thy [was: performance problems]

Hi all, Am 12.09.2018 um 11:12 schrieb Lawrence Paulson: > I regard it as indispensable. But it does need better pretty printing. > Also I greatly prefer the if/for format to assume/fix. Am 12.09.2018 um 12:12 schrieb Mathias Fleury: > I have my own version of explore >

Re: [isabelle-dev] Explorer.thy [was: performance problems]

Hi all, I have my own version of explore (https://bitbucket.org/isafol/isafol/src/master/lib/Explorer.thy ), which does not have better pretty printing, but has two variants that I find indispensable: explore_have produces

Re: [isabelle-dev] Explorer.thy [was: performance problems]

I regard it as indispensable. But it does need better pretty printing. Also I greatly prefer the if/for format to assume/fix. Larry > On 12 Sep 2018, at 07:23, Florian Haftmann > wrote: > >>> On 7 Sep 2018, at 19:18, Makarius wrote: >>> >>> I can't try it out, since theory "Explorer" is

Re: [isabelle-dev] Explorer.thy [was: performance problems]

>> On 7 Sep 2018, at 19:18, Makarius wrote: >> >> I can't try it out, since theory "Explorer" is missing. > > Attached. A very cool thing. Nice to see that old draft from 5 years ago. I would still agree that such a tool would be tremendously useful, but before going into the distro it would