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

[Victor Porton]

05.01.2011, 13:24, "Slawomir Kolodynski" <address@hidden>:
> --- 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.

I did
$ isabelle usedir -b ZF ../../IsarMathLib

and afterward (from the directory ../..):
$ isabelle emacs -p xemacs21 -l IsarMathLib

theory my
  imports Fol1
begin
end

*** Could not find theory file "Fol1.thy" in ".", "/home/porton/math/formal"
*** Theory loader: the error(s) above occurred while examining theory "Fol1"
*** At command "theory".

It does not work.

-- 
Victor Porton - http://portonvictor.org