Re: [isabelle] Reading a proof
- To: John Munroe <munddr at gmail.com>
- Subject: Re: [isabelle] Reading a proof
- From: Makarius <makarius at sketis.net>
- Date: Mon, 3 Oct 2011 11:24:08 +0200 (CEST)
- Cc: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <CAP0k5J5+K8yMFyYNobue623=bbMWmu_4zrvKNSML3yh0UPy12w@mail.gmail.com>
- References: <CAP0k5J6Pf-N_6+He_MJzQPBZNb+Uf5uv8rWYq0b64U0tcpKB5w@mail.gmail.com> <alpine.LNX.email@example.com> <CAP0k5J5+K8yMFyYNobue623=bbMWmu_4zrvKNSML3yh0UPy12w@mail.gmail.com>
- User-agent: Alpine 1.10 (LNX 962 2008-03-14)
On Fri, 30 Sep 2011, John Munroe wrote:
For full proofs the basic HOL image needs to provide them already *and* they
need to be enabled for your own session.
For some years we used to have HOL with proof terms by default, but it
became to huge. You need to build your own image, e.g. like this:
Isabelle2011/build -m HOL-Proofs
This logic image then needs to be selected in PG when starting up.
Thanks. I can start it up with the HOL-Proofs image, but I can't seem
to import RealVector, Real, etc. It says that "Could not find file
"RealVector.thy". Can one use the reals with the HOL-Proofs image?
The HOL-Proofs target in the IsaMakefile merely uses the content of the
HOL-Main session, without type real and complex.
The include the latter you can rebuild the image by imitating the
IsaMakefile entry for it:
isabelle usedir -b -g true -p 2 -q 0 Pure HOL-Proofs
This archive was generated by a fusion of
Pipermail (Mailman edition) and