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.
added listsum lemmas
2010-05-14, by nipkow
Revert mixin patch due to inacceptable performance drop.
2010-05-14, by ballarin
add "no_atp"s to Nitpick lemmas
2010-05-14, by blanchet
query _HOME environment variables at run-time, not at build-time
2010-05-14, by blanchet
move Refute dependency from Plain to Main
2010-05-14, by blanchet
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
2010-05-14, by blanchet
recognize new Kodkod error message syntax
2010-05-14, by blanchet
improve precision of set constructs in Nitpick
2010-05-14, by blanchet
produce more potential counterexamples for subset operator (cf. quantifiers)
2010-05-14, by blanchet
improved Sledgehammer proofs
2010-05-14, by blanchet
pass "full_type" argument to proof reconstruction
2010-05-14, by blanchet
made Sledgehammer's full-typed proof reconstruction work for the first time;
2010-05-14, by blanchet
delect installed ATPs dynamically, _not_ at image built time
2010-05-14, by blanchet
Fix syntax; apparently constant apply was introduced in an earlier changeset.
2010-05-13, by ballarin
Merged.
2010-05-13, by ballarin
Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
2010-05-13, by ballarin
Remove improper use of mixin in class package.
2010-05-13, by ballarin
Multiset: renamed, added and tuned lemmas;
2010-05-13, by nipkow
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
2010-05-12, by huffman
more precise dependencies
2010-05-13, by boehmes
updated SMT certificates
2010-05-12, by boehmes
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-05-12, by boehmes
integrated SMT into the HOL image
2010-05-12, by boehmes
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
2010-05-12, by boehmes
use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)
2010-05-12, by boehmes
split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)
2010-05-12, by boehmes
added tracing of reconstruction data
2010-05-12, by boehmes
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
2010-05-12, by boehmes
deleted SMT translation files (to be replaced by a simplified version)
2010-05-12, by boehmes
move the addition of extra facts into a separate module
2010-05-12, by boehmes
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-30
+30
+50
+100
+300
+1000
+3000
+10000
+30000
tip