[isabelle] typecheck a term



Hi,

I needed to create some Isabelle terms by hand, and would like to make
sure they typecheck as a sanity check.  So, eg.

Const ("==", "bool => bool => bool") $ Free ("a", "bool") $
      Free ("b", "prop") : Term.term

Doesn't typecheck.  What function do I call?

Thanks,

Sean





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