| Fri, 18 Nov 2005 07:10:00 +0100 | mengj | -- terms are fully typed. | changeset | files |
| Fri, 18 Nov 2005 07:08:54 +0100 | mengj | -- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first. | changeset | files |
| Fri, 18 Nov 2005 07:08:18 +0100 | mengj | -- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format. | changeset | files |
| Fri, 18 Nov 2005 07:07:47 +0100 | mengj | -- added combinator reduction axioms (typed and untyped) for HOL goals. | changeset | files |