Re: [isabelle] Finding the instantiation of a variable
On Sun, 18 Jul 2010, Alexander Krauss wrote:
I've tried running 'full_prf' after 'apply auto', but I get an error
about 'minimal proof object' even I have Full Proof switched on in PG.
I am surprised by this myself. I would also have expected a full proof
here. Maybe someone else has an idea?
If this is Isabelle2009-2, then you need to build HOL-Proofs explicitly,
via "Isabelle2009-2/build -m HOL-Proofs" on the command lines.
In the past proof terms used to be part of the default HOL image, but we
had to discontinue that due to resource limitations.
This archive was generated by a fusion of
Pipermail (Mailman edition) and