Re: [isabelle] HOL-Proofs



On 06/13/2013 09:17 AM, Christian Sternagel wrote:
Dear all,

when browsing ~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy using

   isabelle jedit -l HOL-Proofs Higman_Extraction.thy

I get the error

   name_of_thm: bad proof of theorem
   ...

in line 14. What am I missing?

Hi Christian,

looks like you have not switched on proof terms for the current session. You could
try to temporarily add something like

  ML {* proofs := 2 *}

at the beginning of Higman.thy. In ProofGeneral, proof terms can be switched on for
the current session using the Settings menu, but I have no idea how this can be done
in JEdit :-(

Greetings,
Stefan




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