Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers

On 6/28/2012 4:33 PM, Makarius wrote:
Once your session is up and running with one of these images, you need
to enable proof terms again for your interactive session, e.g. like this:

ML {* proofs := 2 *}

Unfortunately, the manuals and the system are not in best shape for
proof terms, because they are so rarely used.

Some examples are in src/HOL/Proofs/.


Thanks for the instructions. In thinking that I should investigate what proof terms can do for me, I think I saw one. It looked like a huge lambda calculus term. It was scary looking, with lots of parentheses. I might check it out someday.


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