Re: [isabelle] Trying to implement conditional skip-proofs, need advice.



Hello Thomas,

have you considered building an image for your completed theories and running Isabelle with this image? This saves you the re-execution time of completed theories.

Here is how you build an image: In the directory with your theories, set up ROOT.ML to include all theories that are supposed to go into the image (add use_thy "MyTheory"; for each of the leaves of your theory tree). Then, execute from within the directory the command

isatool usedir -b HOL myimage

To load the image into Isabelle, use

Isabelle -l myimage

or select myimage from the Proof General menu. You can then load theories that build upon the theories in the image without being required to reload the latter.

HTH,

Nicole






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