Mercurial
Mercurial
>
repos
>
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
src/HOL/Tools/res_atp_setup.ML
Fri, 18 Nov 2005 07:07:47 +0100
mengj
-- added combinator reduction axioms (typed and untyped) for HOL goals.
file
|
diff
|
annotate
Wed, 09 Nov 2005 18:01:33 +0100
paulson
Skolemization by inference, but not quite finished
file
|
diff
|
annotate
Thu, 03 Nov 2005 04:31:12 +0100
mengj
Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names.
file
|
diff
|
annotate
Fri, 28 Oct 2005 17:27:49 +0200
haftmann
circumvented smlnj value restriction
file
|
diff
|
annotate
Fri, 28 Oct 2005 02:27:19 +0200
mengj
Added new functions to handle HOL goals and lemmas.
file
|
diff
|
annotate
Fri, 21 Oct 2005 02:57:22 +0200
mengj
Merged theory ResAtpOracle.thy into ResAtpMethods.thy
file
|
diff
|
annotate
Wed, 19 Oct 2005 10:25:46 +0200
mengj
*** empty log message ***
file
|
diff
|
annotate
Wed, 19 Oct 2005 06:33:24 +0200
mengj
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
file
|
diff
|
annotate
less
more
(0)
tip