Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +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:27:19 +0200 Added new functions to handle HOL goals and lemmas.
changeset
mengj [Fri, 28 Oct 2005 02:27:19 +0200] rev 18001
Added new functions to handle HOL goals and lemmas. Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file. Removed several functions definitions, and combined them with those in other files.
Fri, 28 Oct 2005 02:25:57 +0200 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
mengj [Fri, 28 Oct 2005 02:25:57 +0200] rev 18000
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. Also added function "repeat_RS" to the signature.
Fri, 28 Oct 2005 02:24:58 +0200 Added several functions to the signature.
changeset
mengj [Fri, 28 Oct 2005 02:24:58 +0200] rev 17999
Added several functions to the signature. Added two new functions, which are used by res_hol_clause.ML programs.
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle