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.
-- terms are fully typed.
2005-11-18, by mengj
-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
2005-11-18, by 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.
2005-11-18, by mengj
-- added combinator reduction axioms (typed and untyped) for HOL goals.
2005-11-18, by mengj
-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
2005-11-18, by mengj
-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
2005-11-18, by mengj
-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
2005-11-18, by mengj
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-30
-10
-7
+7
+10
+30
+100
+300
+1000
+3000
+10000
+30000
tip