[isabelle] full proofs



Hi,

  I'm trying to get a proof term for sylow_thm.
I tried "build -m HOL-Algebra HOL", which
compiled a heap, but didn't produce proofs apparently:

theory Tmp = Main + Sylow:

thm sylow_thm

full_prf sylow_thm


*** reconstruct_proof: minimal proof object
*** At command "full_prf".


I set
 proofs:= 2
in
Pure/ROOT.ML
and rebuilt the heap, but this didn't help either

Any suggestions?

Thanks,

Sean






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