Re: [isabelle] Proof sketching in editor buffer [was: RC5: Ordering of normal output and error output]

> 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 MHonArc.