Re: [isabelle] Length of Proofs



On Mon, 19 Nov 2012, Lawrence Paulson wrote:

As I see it, there are advantages to both interfaces. And everything is accessible from ML simply because it is the implementation language, although of course this access may not be very convenient. I think it's generally accepted these days that the ML level really is more appropriate for development than for ordinary reasoning. It isn't realistic to support both Isar and the ML level as the day-to-day user interface; even with unlimited resources, such duplication wouldn't be very elegant.

Actually, the Prover IDE supports both Isabelle/Isar and Isabelle/ML pretty well -- note that Isabelle/ML needs to be distinguished from the ML bootstrapping environment to get the Isabelle/Pure/Isar implementation up and running.

You can even imitate the proof style from the 1990-ies like this:

  apply (tactic {* my_tac @{context} 7 *})

Its definitely not elegant, and there is little reason to use this form today. It is better to use method_setup to define your own application specific proof methods first, and then use them in the proofs.


	Makarius





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