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
boehmes [Wed, 12 May 2010 23:53:54 +0200] rev 36890
normalize numerals: also rewrite Numeral0 into 0
boehmes [Wed, 12 May 2010 23:53:53 +0200] rev 36889
added missing rewrite rules for natural min and max
boehmes [Wed, 12 May 2010 23:53:52 +0200] rev 36888
rewrite bool case expressions as if expression
boehmes [Wed, 12 May 2010 23:53:51 +0200] rev 36887
simplified normalize_rule and moved it further down in the code
boehmes [Wed, 12 May 2010 23:53:50 +0200] rev 36886
merged addition of rules into one function
boehmes [Wed, 12 May 2010 23:53:49 +0200] rev 36885
added simplification for distinctness of small lists
boehmes [Wed, 12 May 2010 23:53:48 +0200] rev 36884
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
wenzelm [Fri, 14 May 2010 19:53:36 +0200] rev 36883
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
wenzelm [Thu, 13 May 2010 21:36:38 +0200] rev 36882
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
wenzelm [Thu, 13 May 2010 21:17:09 +0200] rev 36881
the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;
wenzelm [Thu, 13 May 2010 20:15:59 +0200] rev 36880
avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
wenzelm [Thu, 13 May 2010 18:47:07 +0200] rev 36879
raise Fail uniformly for proofterm errors, which appear to be rather low-level;