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.


	Makarius





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