Re: [isabelle] Printing instantiations



On Thu, 17 Jun 2010, Florian Haftmann wrote:

to inspect proofs, you have to use the image "HOL-Proofs" (containing
proof terms) instead of "HOL" and turn proof objects on by selecting
"Full proofs" from the Isabelle settings menu.

Actually, in the still official Isabelle2009-1 distribution you only need to enable "Full proofs", because the HOL image contains full proofs already.

For the coming Isabelle2009-2 we had to give up that convenience, because HOL proofs have grown too fat, so there will be the separate HOL-Proofs image that has to be build manually.


	Makarius






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