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
-32
+32
+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.
tuned naming
2010-12-21, by haftmann
evaluator separating static and dynamic operations
2010-12-21, by haftmann
canonical handling of theory context argument
2010-12-21, by haftmann
merged
2010-12-21, by haftmann
evaluator separating static and dynamic operations
2010-12-21, by haftmann
program is separate argument to serializer
2010-12-21, by haftmann
more explicit structure for serializer invocation
2010-12-21, by haftmann
merged
2010-12-21, by nipkow
tuned proof
2010-12-21, by nipkow
HOLogic.mk_id
2010-12-21, by haftmann
avoid weird symbols in path
2010-12-21, by blanchet
mechanism to keep SMT input and output files around in Mirabelle
2010-12-21, by blanchet
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
2010-12-21, by blanchet
added "smt_triggers" option to experiment with triggers in Sledgehammer;
2010-12-21, by blanchet
enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day
2010-12-21, by blanchet
Cygwin: Poly/ML 5.4.0 requires libgmp3;
2010-12-20, by wenzelm
updated to polyml-5.4.0;
2010-12-20, by wenzelm
tuned;
2010-12-20, by wenzelm
updated for Poly/ML 5.4.0;
2010-12-20, by wenzelm
merged
2010-12-20, by boehmes
avoid ML structure aliases (especially single-letter abbreviations)
2010-12-20, by boehmes
added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions
2010-12-20, by boehmes
merged
2010-12-20, by huffman
configure domain package to work with HOL option type
2010-12-20, by huffman
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
2010-12-20, by huffman
simplify proofs
2010-12-20, by huffman
beta-reduction simproc uses lemma Abs_cfun_inverse2 instead of beta_cfun, to be more robust against eta-contraction
2010-12-20, by huffman
configure domain package to work with HOL sum type
2010-12-20, by huffman
replace list_map function with an abbreviation
2010-12-20, by huffman
merged
2010-12-20, by blanchet
run SPASS and Vampire in SOS mode only if >= 50 facts are passed -- otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy
2010-12-20, by blanchet
disable feature that was enabled by mistake
2010-12-20, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-32
+32
+50
+100
+300
+1000
+3000
+10000
+30000
tip