isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

merged
2010-05-14, by nipkow
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
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
rewrite bool case expressions as if expression
2010-05-12, by boehmes
simplified normalize_rule and moved it further down in the code
2010-05-12, by boehmes
merged addition of rules into one function
2010-05-12, by boehmes
added simplification for distinctness of small lists
2010-05-12, by boehmes
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
2010-05-12, by boehmes
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
2010-05-14, by wenzelm
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
2010-05-13, by wenzelm
the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;
2010-05-13, by wenzelm
avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
2010-05-13, by wenzelm
raise Fail uniformly for proofterm errors, which appear to be rather low-level;
2010-05-13, by wenzelm
unconstrainT operations on proofs, according to krauss/schropp;
2010-05-13, by wenzelm
added Proofterm.get_name variants according to krauss/schropp;
2010-05-13, by wenzelm
conditional structure SingleAssignment;
2010-05-12, by wenzelm
merged
2010-05-12, by wenzelm
merged
2010-05-12, by haftmann
tuned proofs and fact and class names
2010-05-12, by haftmann
tuned fact collection names and some proofs
2010-05-12, by haftmann
grouped local statements
2010-05-12, by haftmann
tuned test problems
2010-05-12, by haftmann
merged
2010-05-12, by wenzelm
merged
2010-05-12, by nipkow
simplified proof
2010-05-12, by nipkow
modernized specifications;
2010-05-12, by wenzelm
updated/unified some legacy warnings;
2010-05-12, by wenzelm
tuned;
2010-05-12, by wenzelm
do not emit legacy_feature warnings here -- users have no chance to disable them;
2010-05-12, by wenzelm
removed obsolete CVS Ids;
2010-05-12, by wenzelm

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle