| 2010-05-14 |
blanchet |
made Sledgehammer's full-typed proof reconstruction work for the first time;
|
changeset |
files
|
| 2010-05-14 |
blanchet |
delect installed ATPs dynamically, _not_ at image built time
|
changeset |
files
|
| 2010-05-13 |
ballarin |
Fix syntax; apparently constant apply was introduced in an earlier changeset.
|
changeset |
files
|
| 2010-05-13 |
ballarin |
Merged.
|
changeset |
files
|
| 2010-05-13 |
ballarin |
Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
|
changeset |
files
|
| 2010-05-13 |
ballarin |
Remove improper use of mixin in class package.
|
changeset |
files
|
| 2010-05-13 |
nipkow |
Multiset: renamed, added and tuned lemmas;
|
changeset |
files
|
| 2010-05-13 |
huffman |
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
|
changeset |
files
|
| 2010-05-12 |
boehmes |
more precise dependencies
|
changeset |
files
|
| 2010-05-12 |
boehmes |
updated SMT certificates
|
changeset |
files
|
| 2010-05-12 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
changeset |
files
|
| 2010-05-12 |
boehmes |
integrated SMT into the HOL image
|
changeset |
files
|
| 2010-05-12 |
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
|
changeset |
files
|
| 2010-05-12 |
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)
|
changeset |
files
|
| 2010-05-12 |
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)
|
changeset |
files
|
| 2010-05-12 |
boehmes |
added tracing of reconstruction data
|
changeset |
files
|
| 2010-05-12 |
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
|
changeset |
files
|
| 2010-05-12 |
boehmes |
deleted SMT translation files (to be replaced by a simplified version)
|
changeset |
files
|
| 2010-05-12 |
boehmes |
move the addition of extra facts into a separate module
|
changeset |
files
|
| 2010-05-12 |
boehmes |
normalize numerals: also rewrite Numeral0 into 0
|
changeset |
files
|
| 2010-05-12 |
boehmes |
added missing rewrite rules for natural min and max
|
changeset |
files
|
| 2010-05-12 |
boehmes |
rewrite bool case expressions as if expression
|
changeset |
files
|
| 2010-05-12 |
boehmes |
simplified normalize_rule and moved it further down in the code
|
changeset |
files
|
| 2010-05-12 |
boehmes |
merged addition of rules into one function
|
changeset |
files
|
| 2010-05-12 |
boehmes |
added simplification for distinctness of small lists
|
changeset |
files
|
| 2010-05-12 |
boehmes |
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
|
changeset |
files
|
| 2010-05-14 |
wenzelm |
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
|
changeset |
files
|
| 2010-05-13 |
wenzelm |
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
|
changeset |
files
|
| 2010-05-13 |
wenzelm |
the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;
|
changeset |
files
|
| 2010-05-13 |
wenzelm |
avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
|
changeset |
files
|
| 2010-05-13 |
wenzelm |
raise Fail uniformly for proofterm errors, which appear to be rather low-level;
|
changeset |
files
|
| 2010-05-13 |
wenzelm |
unconstrainT operations on proofs, according to krauss/schropp;
|
changeset |
files
|
| 2010-05-13 |
wenzelm |
added Proofterm.get_name variants according to krauss/schropp;
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
conditional structure SingleAssignment;
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
merged
|
changeset |
files
|
| 2010-05-12 |
haftmann |
merged
|
changeset |
files
|
| 2010-05-12 |
haftmann |
tuned proofs and fact and class names
|
changeset |
files
|
| 2010-05-12 |
haftmann |
tuned fact collection names and some proofs
|
changeset |
files
|
| 2010-05-12 |
haftmann |
grouped local statements
|
changeset |
files
|
| 2010-05-12 |
haftmann |
tuned test problems
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
merged
|
changeset |
files
|
| 2010-05-12 |
nipkow |
merged
|
changeset |
files
|
| 2010-05-12 |
nipkow |
simplified proof
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
updated/unified some legacy warnings;
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
tuned;
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
do not emit legacy_feature warnings here -- users have no chance to disable them;
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
removed obsolete CVS Ids;
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
removed some obsolete admin stuff;
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
check NEWS;
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
removed obsolete CVS Ids;
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
updated some version numbers;
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
minor tuning;
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only;
|
changeset |
files
|
| 2010-05-12 |
wenzelm |
merged
|
changeset |
files
|
| 2010-05-12 |
haftmann |
merged
|
changeset |
files
|
| 2010-05-12 |
haftmann |
modernized specifications; tuned reification
|
changeset |
files
|
| 2010-05-12 |
haftmann |
merged
|
changeset |
files
|
| 2010-05-12 |
haftmann |
added lemmas concerning last, butlast, insort
|
changeset |
files
|
| 2010-05-12 |
Cezary Kaliszyk |
Remove RANGE_WARN
|
changeset |
files
|