Re: [isabelle] Trying to implement conditional skip-proofs, need advice.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and