Mercurial Mercurial > repos > isabelle / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -10000 -3000 -1000 -300 -100 -30 -10 -8 +8 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
Fri, 28 Oct 2005 02:30:53 +0200 mengj Added Tools/res_hol_clause.ML changeset | files
Fri, 28 Oct 2005 02:30:12 +0200 mengj Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses. changeset | files
Fri, 28 Oct 2005 02:29:01 +0200 mengj Added "writeln_strs" to the signature changeset | files
Fri, 28 Oct 2005 02:28:20 +0200 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. changeset | files
Fri, 28 Oct 2005 02:27:19 +0200 mengj Added new functions to handle HOL goals and lemmas. changeset | files
Fri, 28 Oct 2005 02:25:57 +0200 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. changeset | files
Fri, 28 Oct 2005 02:24:58 +0200 mengj Added several functions to the signature. changeset | files
Fri, 28 Oct 2005 02:23:49 +0200 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. changeset | files
(0) -10000 -3000 -1000 -300 -100 -30 -10 -8 +8 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle