2005-10-28 mengj Added "writeln_strs" to the signature
2005-10-28 mengj Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.
2005-10-28 mengj Added new functions to handle HOL goals and lemmas.
2005-10-28 mengj Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
2005-10-28 mengj Added several functions to the signature.
2005-10-28 mengj A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
2005-10-27 paulson sorted lemma lists
2005-10-27 wenzelm * HOL: alternative iff syntax;
2005-10-27 wenzelm consts: monomorphic;
2005-10-27 wenzelm removed inappropriate monomorphic test;
2005-10-27 wenzelm replaced Defs.monomorphic by Sign.monomorphic;
2005-10-27 wenzelm alternative iff syntax for equality on booleans, with print_mode 'iff';
2005-10-27 haftmann added module Pure/General/rat.ML
2005-10-26 paulson tidied away duplicate thm
Loading...
(0) -10000 -3000 -1000 -300 -100 -14 +14 +100 +300 +1000 +3000 +10000 +30000 tip