| Wed, 12 May 2010 23:54:01 +0200 |
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
|
| Wed, 12 May 2010 23:54:00 +0200 |
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
|
| Wed, 12 May 2010 23:53:59 +0200 |
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
|
| Wed, 12 May 2010 23:53:58 +0200 |
boehmes |
added tracing of reconstruction data
|
changeset |
files
|
| Wed, 12 May 2010 23:53:57 +0200 |
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
|
| Wed, 12 May 2010 23:53:56 +0200 |
boehmes |
deleted SMT translation files (to be replaced by a simplified version)
|
changeset |
files
|
| Wed, 12 May 2010 23:53:55 +0200 |
boehmes |
move the addition of extra facts into a separate module
|
changeset |
files
|
| Wed, 12 May 2010 23:53:54 +0200 |
boehmes |
normalize numerals: also rewrite Numeral0 into 0
|
changeset |
files
|
| Wed, 12 May 2010 23:53:53 +0200 |
boehmes |
added missing rewrite rules for natural min and max
|
changeset |
files
|
| Wed, 12 May 2010 23:53:52 +0200 |
boehmes |
rewrite bool case expressions as if expression
|
changeset |
files
|
| Wed, 12 May 2010 23:53:51 +0200 |
boehmes |
simplified normalize_rule and moved it further down in the code
|
changeset |
files
|
| Wed, 12 May 2010 23:53:50 +0200 |
boehmes |
merged addition of rules into one function
|
changeset |
files
|
| Wed, 12 May 2010 23:53:49 +0200 |
boehmes |
added simplification for distinctness of small lists
|
changeset |
files
|
| Wed, 12 May 2010 23:53:48 +0200 |
boehmes |
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
|
changeset |
files
|
| Fri, 14 May 2010 19:53:36 +0200 |
wenzelm |
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
|
changeset |
files
|
| Thu, 13 May 2010 21:36:38 +0200 |
wenzelm |
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
|
changeset |
files
|
| Thu, 13 May 2010 21:17:09 +0200 |
wenzelm |
the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;
|
changeset |
files
|
| Thu, 13 May 2010 20:15:59 +0200 |
wenzelm |
avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
|
changeset |
files
|
| Thu, 13 May 2010 18:47:07 +0200 |
wenzelm |
raise Fail uniformly for proofterm errors, which appear to be rather low-level;
|
changeset |
files
|
| Thu, 13 May 2010 18:22:10 +0200 |
wenzelm |
unconstrainT operations on proofs, according to krauss/schropp;
|
changeset |
files
|
| Thu, 13 May 2010 17:25:53 +0200 |
wenzelm |
added Proofterm.get_name variants according to krauss/schropp;
|
changeset |
files
|
| Wed, 12 May 2010 22:43:05 +0200 |
wenzelm |
conditional structure SingleAssignment;
|
changeset |
files
|
| Wed, 12 May 2010 17:10:53 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 12 May 2010 15:31:43 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 12 May 2010 15:27:15 +0200 |
haftmann |
tuned proofs and fact and class names
|
changeset |
files
|
| Wed, 12 May 2010 13:51:22 +0200 |
haftmann |
tuned fact collection names and some proofs
|
changeset |
files
|
| Wed, 12 May 2010 12:31:52 +0200 |
haftmann |
grouped local statements
|
changeset |
files
|
| Wed, 12 May 2010 12:31:51 +0200 |
haftmann |
tuned test problems
|
changeset |
files
|
| Wed, 12 May 2010 16:45:59 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 12 May 2010 15:25:23 +0200 |
nipkow |
merged
|
changeset |
files
|