[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Isarmathlib-devel] How to configure Isabelle to use IsarMathLib
From: |
Slawomir Kolodynski |
Subject: |
Re: [Isarmathlib-devel] How to configure Isabelle to use IsarMathLib |
Date: |
Wed, 5 Jan 2011 02:24:29 -0800 (PST) |
--- 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