[isabelle-dev] Converting existing proofs from apply-style to "structured" Isar-style

[Makarius]

On Mon, 16 Sep 2013, Josh Tilles wrote:

> Interesting—I had assumed that changing the proof of a lemma and/or 
> theorem had no functional impact on the code once said lemma/theorem had 
> been verified. Am I incorrect about that? (If the explanation is 
> complicated, please don't feel obligated to go into complete detail. A 
> one-word answer will tell me all I probably *need* to know. Any further 
> explanation would just be to satisfy my beginner's curiosity)

Main Isabelle/HOL is a bottle neck in several respects, even just the 
performance of doing the proofs (with or without explicit proof terms).

Below its Main theory any change requires someone with a few years of 
experience to make non-trivial changes -- otherwise the bootstrap process 
might get affected one way or the other.  Between Main and Complex_Main it 
is a bit easier, but a change there still requires to rebuild almost 
anything else (this takes about 1-2h these days, where such things are 
really fast compared to past times).

It is much more relaxed and fun to look through outlying, presently hardly 
maintained areas, where some gems might be uncovered without getting into 
technical difficulties.

In preparation of the Isabelle2013-1 release, I am myself training my 
fingers (and testing the Prover IDE real-time dynamics) on 
HOL/Multivariate_Analysis.  These huge and mostly unformatted theories now 
work out rather smoothly, even on my old 2-core MacBook Pro.


 	Makarius