Re: [isabelle] avoid rechecking an imported theory




theory test imports myTheory1 myTheory2
  begin ..
How to avoid rechecking the two theories?

You could do it like that: in a file called "ROOT.ML" you have
/----------------------------------------------------\
use_thys ["myTheory1", "myTheory2"];
\----------------------------------------------------/

Then
$ isabelle usedir -b HOL myTheory12

creates a binary myTheory12 based on HOL, which afterwards can be called in "test.thy" as follows
/----------------------------------------------------\

theory test imports myTheory12
 begin ..

\----------------------------------------------------/
where myTheory12 fetches the binary without evaluating the respective theories.

PS1: the above identifiers do not conform to Isabelle standards;
        see doc/implementation.pdf   p.3 section 0.1.2. Naming conventions
PS2: $ find -name ROOT.ML
        will tell you further examples






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