[isabelle] HOL-Proofs



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?

cheers

chris




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