Re: [Isarmathlib-devel] How to configure Isabelle to use IsarMathLib

[Slawomir Kolodynski]

--- On Tue, 1/4/11, Victor Porton <address@hidden> wrote:

> How to make Isabelle and ProofGeneral to use IsarMathLib? I
> want to import theories from IsarMathLib and make use of
> "Find Theorems" feature of ProofGeneral.
> 

Start ProofGeneral in the IsarMathLib directory (where the theory files are).
In your file write 

theory mytheory imports func1

and process that. That will check and make available for searching 
IsarMathLib's func1.thy and all theory files that depend on it.

There is an alternative method where you create a "heap image". This is like a 
binary with all proven theorems. You use it by selecting from ProofGeneral 
instead of ZF logic. The method is described at 
http://www.cl.cam.ac.uk/research/hvg/Isabelle/faq.html .
I haven't used it for a long time.

slawekk