Fri, 14 May 2010 11:24:49 +0200 blanchet improved Sledgehammer proofs
Fri, 14 May 2010 11:24:14 +0200 blanchet pass "full_type" argument to proof reconstruction
Fri, 14 May 2010 11:23:42 +0200 blanchet made Sledgehammer's full-typed proof reconstruction work for the first time;
Fri, 14 May 2010 11:20:09 +0200 blanchet delect installed ATPs dynamically, _not_ at image built time
Thu, 13 May 2010 15:09:42 +0200 ballarin Fix syntax; apparently constant apply was introduced in an earlier changeset.
Thu, 13 May 2010 14:47:15 +0200 ballarin Merged.
Thu, 13 May 2010 13:30:16 +0200 ballarin Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
Thu, 13 May 2010 13:29:43 +0200 ballarin Remove improper use of mixin in class package.
Thu, 13 May 2010 14:34:05 +0200 nipkow Multiset: renamed, added and tuned lemmas;
Wed, 12 May 2010 22:33:10 -0700 huffman use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
Thu, 13 May 2010 00:44:48 +0200 boehmes more precise dependencies
Wed, 12 May 2010 23:54:06 +0200 boehmes updated SMT certificates
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
Wed, 12 May 2010 23:54:02 +0200 boehmes integrated SMT into the HOL image
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
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)
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)
Wed, 12 May 2010 23:53:58 +0200 boehmes added tracing of reconstruction data
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
Wed, 12 May 2010 23:53:56 +0200 boehmes deleted SMT translation files (to be replaced by a simplified version)
Wed, 12 May 2010 23:53:55 +0200 boehmes move the addition of extra facts into a separate module
Wed, 12 May 2010 23:53:54 +0200 boehmes normalize numerals: also rewrite Numeral0 into 0
Wed, 12 May 2010 23:53:53 +0200 boehmes added missing rewrite rules for natural min and max
Wed, 12 May 2010 23:53:52 +0200 boehmes rewrite bool case expressions as if expression
Wed, 12 May 2010 23:53:51 +0200 boehmes simplified normalize_rule and moved it further down in the code
Wed, 12 May 2010 23:53:50 +0200 boehmes merged addition of rules into one function
Wed, 12 May 2010 23:53:49 +0200 boehmes added simplification for distinctness of small lists
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)
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;
Thu, 13 May 2010 21:36:38 +0200 wenzelm conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
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;
Thu, 13 May 2010 20:15:59 +0200 wenzelm avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
Thu, 13 May 2010 18:47:07 +0200 wenzelm raise Fail uniformly for proofterm errors, which appear to be rather low-level;
Thu, 13 May 2010 18:22:10 +0200 wenzelm unconstrainT operations on proofs, according to krauss/schropp;
Thu, 13 May 2010 17:25:53 +0200 wenzelm added Proofterm.get_name variants according to krauss/schropp;
Wed, 12 May 2010 22:43:05 +0200 wenzelm conditional structure SingleAssignment;
Wed, 12 May 2010 17:10:53 +0200 wenzelm merged
Wed, 12 May 2010 15:31:43 +0200 haftmann merged
Wed, 12 May 2010 15:27:15 +0200 haftmann tuned proofs and fact and class names
Wed, 12 May 2010 13:51:22 +0200 haftmann tuned fact collection names and some proofs
Wed, 12 May 2010 12:31:52 +0200 haftmann grouped local statements
Wed, 12 May 2010 12:31:51 +0200 haftmann tuned test problems
Wed, 12 May 2010 16:45:59 +0200 wenzelm merged
Wed, 12 May 2010 15:25:23 +0200 nipkow merged
Wed, 12 May 2010 15:25:02 +0200 nipkow simplified proof
Wed, 12 May 2010 16:44:49 +0200 wenzelm modernized specifications;
Wed, 12 May 2010 15:25:58 +0200 wenzelm updated/unified some legacy warnings;
Wed, 12 May 2010 15:23:38 +0200 wenzelm tuned;
Wed, 12 May 2010 14:52:23 +0200 wenzelm do not emit legacy_feature warnings here -- users have no chance to disable them;
Wed, 12 May 2010 14:17:26 +0200 wenzelm removed obsolete CVS Ids;
Wed, 12 May 2010 14:02:50 +0200 wenzelm removed some obsolete admin stuff;
Wed, 12 May 2010 14:02:19 +0200 wenzelm check NEWS;
Wed, 12 May 2010 13:54:49 +0200 wenzelm removed obsolete CVS Ids;
Wed, 12 May 2010 13:52:34 +0200 wenzelm updated some version numbers;
Wed, 12 May 2010 13:34:24 +0200 wenzelm minor tuning;
Wed, 12 May 2010 13:21:23 +0200 wenzelm reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only;
Wed, 12 May 2010 12:51:32 +0200 wenzelm merged
Wed, 12 May 2010 12:20:16 +0200 haftmann merged
Wed, 12 May 2010 12:09:28 +0200 haftmann modernized specifications; tuned reification
Wed, 12 May 2010 11:18:42 +0200 haftmann merged
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip