Re: [isabelle] Reading a proof
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and