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