[isabelle-dev] sledgehammer

[Makarius]

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