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

>> Some time (years?) ago I did a small sketch of a command which takes a
>> method, applies and it writes back the resulting goal state as Isar
>> skeleton.  
> Sounds like a good idea that may save lot's of tedious copy-and-paste if
> you already have the detailed proof in mind, and want to document the
> steps at a very fine-grained level in Isar.

I really had proof exploration in mind.

> I am unsure whether it would work as a replacement for proof-exploration
> as described above, because it would produce lots of text in the main
> buffer, which may obfuscate the whole proof, in particular for big
> subgoals. (I regularly have ~20 subgoals, each of which is ~20 lines
> long)

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.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.