Re: [isabelle] Proof sketching in editor buffer [was: RC5: Ordering of normal output and error output]
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Proof sketching in editor buffer [was: RC5: Ordering of normal output and error output]
- From: Peter Lammich <lammich at in.tum.de>
- Date: Wed, 03 Jun 2015 09:24:06 +0200
- In-reply-to: <556E0434.email@example.com>
- References: <1432210096.24892.48.camel@lapnipkow10> <CAGbqCMyoFeJon19y7=PW9Po-CZ-WKyTha3yzGZdDXEqbYz52kA@mail.gmail.com> <alpine.LNX.firstname.lastname@example.org> <1432508339.21362.10.camel@lapnipkow10> <alpine.LNX.email@example.com> <5564CCB5.firstname.lastname@example.org> <1432713587.21362.32.camel@lapnipkow10> <556E0434.email@example.com>
> Deleting big experimental sections should not be a big problem.
> When doing proof development nowadays, I often make the experience that,
> when I am actually finishing the proof, I have to delete draft lines
> more than an editor page (!) which has accumulated over time.
The same for me.
My fear was, if these draft lines now also contain tons of subgoals,
they may be dozens of editor pages, and obfuscate the essential proof
steps that have been worked out. But, maybe I've not correctly
understood the idea.
This archive was generated by a fusion of
Pipermail (Mailman edition) and