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?

Thanks

John

>
>
>        Makarius
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.