nipkow [Fri, 14 May 2010 22:46:41 +0200] rev 36920
added listsum lemmas
ballarin [Fri, 14 May 2010 21:23:29 +0200] rev 36919
Revert mixin patch due to inacceptable performance drop.
blanchet [Fri, 14 May 2010 15:27:07 +0200] rev 36918
add "no_atp"s to Nitpick lemmas
blanchet [Fri, 14 May 2010 15:26:26 +0200] rev 36917
query _HOME environment variables at run-time, not at build-time
blanchet [Fri, 14 May 2010 15:09:37 +0200] rev 36916
move Refute dependency from Plain to Main
blanchet [Fri, 14 May 2010 15:07:53 +0200] rev 36915
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet [Fri, 14 May 2010 15:02:38 +0200] rev 36914
recognize new Kodkod error message syntax
blanchet [Fri, 14 May 2010 14:14:22 +0200] rev 36913
improve precision of set constructs in Nitpick
blanchet [Fri, 14 May 2010 12:01:16 +0200] rev 36912
produce more potential counterexamples for subset operator (cf. quantifiers)
blanchet [Fri, 14 May 2010 11:24:49 +0200] rev 36911
improved Sledgehammer proofs
blanchet [Fri, 14 May 2010 11:24:14 +0200] rev 36910
pass "full_type" argument to proof reconstruction
blanchet [Fri, 14 May 2010 11:23:42 +0200] rev 36909
made Sledgehammer's full-typed proof reconstruction work for the first time;
previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code
blanchet [Fri, 14 May 2010 11:20:09 +0200] rev 36908
delect installed ATPs dynamically, _not_ at image built time
ballarin [Thu, 13 May 2010 15:09:42 +0200] rev 36907
Fix syntax; apparently constant apply was introduced in an earlier changeset.
ballarin [Thu, 13 May 2010 14:47:15 +0200] rev 36906
Merged.
ballarin [Thu, 13 May 2010 13:30:16 +0200] rev 36905
Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
ballarin [Thu, 13 May 2010 13:29:43 +0200] rev 36904
Remove improper use of mixin in class package.
nipkow [Thu, 13 May 2010 14:34:05 +0200] rev 36903
Multiset: renamed, added and tuned lemmas;
Permutation: replaced local "remove" by List.remove1
huffman [Wed, 12 May 2010 22:33:10 -0700] rev 36902
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
boehmes [Thu, 13 May 2010 00:44:48 +0200] rev 36901
more precise dependencies
boehmes [Wed, 12 May 2010 23:54:06 +0200] rev 36900
updated SMT certificates
boehmes [Wed, 12 May 2010 23:54:04 +0200] rev 36899
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes [Wed, 12 May 2010 23:54:02 +0200] rev 36898
integrated SMT into the HOL image
boehmes [Wed, 12 May 2010 23:54:01 +0200] rev 36897
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
boehmes [Wed, 12 May 2010 23:54:00 +0200] rev 36896
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)
boehmes [Wed, 12 May 2010 23:53:59 +0200] rev 36895
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)
boehmes [Wed, 12 May 2010 23:53:58 +0200] rev 36894
added tracing of reconstruction data
boehmes [Wed, 12 May 2010 23:53:57 +0200] rev 36893
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
boehmes [Wed, 12 May 2010 23:53:56 +0200] rev 36892
deleted SMT translation files (to be replaced by a simplified version)
boehmes [Wed, 12 May 2010 23:53:55 +0200] rev 36891
move the addition of extra facts into a separate module