[isabelle-dev] sledgehammer

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


More information about the isabelle-dev mailing list