Re: [isabelle] THY path



Hi Chris,

>>  To get to work quickly, I simply load these base theories with the
> > "skip proof" option enabled, which is fairly fast.
> well ^that sounds interesting... <whispering>how do I activate it?</whispering>
1. Start ProofGeneral
2. Start Isabelle (C-c C-s)
3. Menu Isabelle -> Settings -> Skip proof
4. Process the theories up to the point you want to start working on
5. Deactivate skip proof again

In the "Skip proof"-mode, Isabelle skips all proofs, but not the definitions, context switches, attribute declarations, etc, i.e. the latter take still their time to be processed.

Another option to get started quickly is to use writeable heaps, where you can start right where you had stopped before. I used to work with these, but my heaps got so large that shutting down Isabelle and writing the heap back to the disk exceeded all emacs timeouts. Makarius might be able to tell you more about writeable heaps.

Andreas






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