[isabelle] rep_thm



Hello,

  I'm having trouble examining proof terms from the Isabelle top level.
Any nontrivial proof seems to crash both polyml and smlnj.
I tried this with proofs set to both 2 and 1.   Could this
be a product of my particular setup, or do all machine arrangements
make the program crash?

eg.

ML {* val {prop, der=(_, prf), sign, ...} =
  rep_thm (thm "less_max_iff_disj") *}

This is only 50K lines in the xml output (one tag per line), so it doesn't seem like
it should be a memory problem.

Thanks,

Sean





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