20130418 
wenzelm 
20130418 
simplifier uses proper Proof.context instead of historic type simpset;

file  diff  annotate 
20121031 
blanchet 
20121031 
soft SMT timeout

file  diff  annotate 
20120215 
wenzelm 
20120215 
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;

file  diff  annotate 
20120214 
wenzelm 
20120214 
normalized aliases;

file  diff  annotate 
20111107 
boehmes 
20111107 
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambdalifting can be instantiated in different ways

file  diff  annotate 
20111107 
boehmes 
20111107 
replace higherorder matching against schematic theorem with dedicated reconstruction method

file  diff  annotate 
20111028 
wenzelm 
20111028 
tuned Named_Thms: proper binding;

file  diff  annotate 
20110912 
nipkow 
20110912 
new fastforce replacing fastsimp  less confusing name

file  diff  annotate 
20110825 
boehmes 
20110825 
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization

file  diff  annotate 
20110808 
wenzelm 
20110808 
misc tuning  eliminated oldfashioned rep_thm;

file  diff  annotate 
20110718 
boehmes 
20110718 
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)

file  diff  annotate 
20110526 
boehmes 
20110526 
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling ifthenelse from below uninterpreted constants (suggested by Jasmin Christian Blanchette)

file  diff  annotate 
20110513 
wenzelm 
20110513 
proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;

file  diff  annotate 
20110416 
wenzelm 
20110416 
modernized structure Proof_Context;

file  diff  annotate 
20110408 
boehmes 
20110408 
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables

file  diff  annotate 
20110401 
boehmes 
20110401 
save reflexivity steps in discharging Z3 Skolemization hypotheses

file  diff  annotate 
20110401 
boehmes 
20110401 
reimplemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higherorder resolution do most of the work in the end

file  diff  annotate 
20110309 
boehmes 
20110309 
finished and tested Z3 proof reconstruction for injective functions;
only treat variables as atomic, and especially abstract constants (Isabelle's interpretation of these constants is most likely not known to Z3 and thus irrelevant for the proof)

file  diff  annotate 
20110103 
boehmes 
20110103 
reimplemented support for datatypes (including records and typedefs);
added test cases for datatypes, records and typedefs

file  diff  annotate 
20101220 
boehmes 
20101220 
avoid ML structure aliases (especially singleletter abbreviations)

file  diff  annotate 
20101215 
boehmes 
20101215 
the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils

file  diff  annotate 
20101215 
boehmes 
20101215 
fixed proof reconstruction for lambdalifted problems (which broke when the lambdalifting code was changed to operate on terms instead of on theorems)

file  diff  annotate 
20101215 
boehmes 
20101215 
adapted the Z3 proof parser to recent changes in Z3's proof format;
keep the proof steps in an ordered list instead of in an Inttab (simplifies proof reconstruction code)

file  diff  annotate 
20101215 
boehmes 
20101215 
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
abolished SMT interface concept in favor of solver classes (now also the translation configuration is stored in the context);
proof reconstruction is now expected to return a theorem stating False (and hence needs to discharge all hypothetical definitions);
builtin functions carry additionally their arity and their most general type;
slightly generalized the definition of fun_app

file  diff  annotate 
20101124 
boehmes 
20101124 
be more precise: only treat constant 'distinct' applied to an explicit list as builtin

file  diff  annotate 
20101124 
boehmes 
20101124 
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)

file  diff  annotate 
20101122 
boehmes 
20101122 
added support for quantifier weight annotations

file  diff  annotate 
20101122 
boehmes 
20101122 
share and use more utility functions;
slightly reduced complexity for Z3 proof rule 'rewrite'

file  diff  annotate 
20101122 
boehmes 
20101122 
added prove reconstruction for injective functions;
added SMT_Utils to collect frequently used functions

file  diff  annotate 
20101117 
boehmes 
20101117 
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)

file  diff  annotate 
20101112 
boehmes 
20101112 
preliminary support for newer versions of Z3

file  diff  annotate 
20101108 
boehmes 
20101108 
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)

file  diff  annotate 
20101029 
boehmes 
20101029 
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list

file  diff  annotate 
20101026 
boehmes 
20101026 
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)

file  diff  annotate 
20101026 
boehmes 
20101026 
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface

file  diff  annotate 
20101026 
boehmes 
20101026 
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs

file  diff  annotate 
20100920 
wenzelm 
20100920 
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;

file  diff  annotate 
20100901 
haftmann 
20100901 
replaced Table.map' by Table.map

file  diff  annotate 
20100827 
haftmann 
20100827 
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj

file  diff  annotate 
20100526 
boehmes 
20100526 
try logical and theory abstraction before full abstraction (avoids warnings of linarith)

file  diff  annotate 
20100515 
wenzelm 
20100515 
incorporated further conversions and conversionals, after some minor tuning;

file  diff  annotate 
20100512 
boehmes 
20100512 
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable

file  diff  annotate 
20100512 
boehmes 
20100512 
integrated SMT into the HOL image

file  diff  annotate 