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
minimalistic tuning.
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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
