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
-24
+24
+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.
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
normalize numerals: also rewrite Numeral0 into 0
2010-05-12, by boehmes
added missing rewrite rules for natural min and max
2010-05-12, by boehmes
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-24
+24
+50
+100
+300
+1000
+3000
+10000
+30000
tip