makarius at sketis.net
Tue Sep 24 22:15:47 CEST 2013
On Mon, 2 Sep 2013, Lawrence Paulson wrote:
> I agree that the generated proof should start on a fresh line, because
> these calls are often quite lengthy text strings.
The fresh line is there in Isabelle/88c6e630c15f but it is merely
The concept that is missing here is some structural editing of the text:
copy-pasting sub-proofs should somehow take the structure into account,
with proper whitespace, line breaks and indentation according to Isar.
That's left for a future release.
More information about the isabelle-dev