Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-30
-10
-7
+7
+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
.
The revision graph only works with JavaScript-enabled browsers.
reachable - abandoned foldl_map in favor of fold_map
2005-10-28, by haftmann
Added Tools/res_hol_clause.ML
2005-10-28, by mengj
Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
2005-10-28, by mengj
Added "writeln_strs" to the signature
2005-10-28, by 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, by mengj
Added new functions to handle HOL goals and lemmas.
2005-10-28, by 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, by mengj
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-30
-10
-7
+7
+10
+30
+100
+300
+1000
+3000
+10000
+30000
tip