Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-30
+30
+50
+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.
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
2010-10-24, by huffman
rename constant 'one_when' to 'one_case'
2010-10-24, by huffman
merged
2010-10-27, by haftmann
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
2010-10-27, by haftmann
regenerated keyword file
2010-10-27, by krauss
made SML/NJ happy
2010-10-27, by boehmes
adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
2010-10-26, by blanchet
better list of irrelevant SMT constants
2010-10-26, by blanchet
if "debug" is on, print list of relevant facts (poweruser request);
2010-10-26, by blanchet
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
2010-10-26, by blanchet
"Nitpick" -> "Sledgehammer";
2010-10-26, by blanchet
merge
2010-10-26, by blanchet
merged
2010-10-26, by blanchet
remove needless context argument;
2010-10-26, by blanchet
use proper context
2010-10-26, by boehmes
trace assumptions before giving them to the SMT solver
2010-10-26, by boehmes
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
2010-10-26, by boehmes
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
2010-10-26, by boehmes
include ATP in theory List -- avoid theory edge by-passing the prominent list theory
2010-10-26, by haftmann
fixed typo
2010-10-26, by krauss
merged
2010-10-26, by blanchet
merged
2010-10-26, by blanchet
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
2010-10-26, by blanchet
tuning
2010-10-26, by blanchet
merged
2010-10-26, by haftmann
consider base sorts of superclasses simultaneously during processing of class specification -- avoids clash of different base sorts
2010-10-26, by haftmann
more general treatment of type argument in code certificates for operations on abstract types
2010-10-26, by haftmann
partial_function is a declaration command
2010-10-26, by haftmann
merged
2010-10-26, by blanchet
proper error handling for SMT solvers in Sledgehammer
2010-10-26, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-30
+30
+50
+100
+300
+1000
+3000
+10000
+30000
tip