20140321 
wenzelm 
20140321 
more qualified names;

file  diff  annotate 
20140212 
blanchet 
20140212 
renamed '{prod,sum,bool,unit}_case' to 'case_...'

file  diff  annotate 
20131231 
wenzelm 
20131231 
proper context for norm_hhf and derived operations;
clarified tool context in some boundary cases;

file  diff  annotate 
20131119 
haftmann 
20131119 
eliminiated neg_numeral in favour of  (numeral _)

file  diff  annotate 
20131110 
haftmann 
20131110 
simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number

file  diff  annotate 
20131002 
blanchet 
20131002 
make SMT integration slacker w.r.t. bad apples (facts)

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

file  diff  annotate 
20130328 
boehmes 
20130328 
new, simpler implementation of monomorphization;
old monomorphization code is still available as Legacy_Monomorphization;
modified SMT integration to use the new monomorphization code

file  diff  annotate 
20121221 
boehmes 
20121221 
refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of naturalnumber constants might leave some of them untouched)

file  diff  annotate 
20120330 
huffman 
20120330 
move lemmas from Nat_Numeral to Int.thy and Num.thy

file  diff  annotate 
20120327 
boehmes 
20120327 
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct

file  diff  annotate 
20120325 
huffman 
20120325 
merged fork with new numeral representation (see NEWS)

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 
20110912 
nipkow 
20110912 
new fastforce replacing fastsimp  less confusing name

file  diff  annotate 
20110905 
boehmes 
20110905 
tuned

file  diff  annotate 
20110531 
boehmes 
20110531 
use new monomorphizer for SMT;
simplify the monomorphizer by inlining functions and proper passing of arguments

file  diff  annotate 
20110416 
wenzelm 
20110416 
modernized structure Proof_Context;

file  diff  annotate 
20110401 
boehmes 
20110401 
make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option

file  diff  annotate 
20110331 
boehmes 
20110331 
provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)

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

file  diff  annotate 
20101220 
boehmes 
20101220 
added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions

file  diff  annotate 
20101220 
boehmes 
20101220 
perform monomorphization during normalization: schematic numerals might be monomorphized into builtin numerals and then numeral normalization is required

file  diff  annotate 
20101219 
boehmes 
20101219 
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
hide internal constants z3div and z3mod;
rewrite div/mod to z3div/z3mod instead of adding extra rules characterizing div/mod in terms of z3div/z3mod

file  diff  annotate 
20101217 
wenzelm 
20101217 
tuned;

file  diff  annotate 
20101216 
paulson 
20101216 
merged

file  diff  annotate 
20101216 
paulson 
20101216 
made sml/nj happy

file  diff  annotate 
20101215 
boehmes 
20101215 
fixed trigger inference: testing if a theorem already has a trigger was too strict;
fixed monomorphization with respect to triggers (which might occur schematically)

file  diff  annotate 
20101215 
boehmes 
20101215 
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)

file  diff  annotate 
20101215 
boehmes 
20101215 
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
added simple trigger inference mechanism;
added syntactic checks for triggers and quantifier weights;
factored out the normalization of special quantifiers (used to be in the etanormalization part);
normalization now unfolds abs/min/max (not SMTLIBspecific);
rules for pairs and function update are not anymore added automatically to the problem;
more aggressive rewriting of natural number operations into integer operations (minimizes the number of remaining natint coercions);
normalizations are now managed in a classbased manner (similar to builtin symbols)

file  diff  annotate 
20101208 
boehmes 
20101208 
be more flexible: store SMT builtin symbols in generic contexts (not in theory contexts)

file  diff  annotate 
20101207 
boehmes 
20101207 
centralized handling of builtin types and constants;
also store types and constants which are rewritten during preprocessing;
interfaces are identified by classes (supporting inheritance, at least on the level of builtin symbols);
removed term_eq in favor of type replacements: termlevel occurrences of type bool are replaced by type term_bool (only for the translation)

file  diff  annotate 
20101124 
boehmes 
20101124 
swap names for builtin tester functions (to better reflect the intuition of what they do);
etaexpand all builtin functions (even those which are only partially supported)

file  diff  annotate 
20101124 
boehmes 
20101124 
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)

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

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

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 
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 
etaexpand builtin constants; also rewrite partially applied natural number terms

file  diff  annotate 
20101029 
boehmes 
20101029 
optionally drop assumptions which cannot be preprocessed

file  diff  annotate 
20101029 
boehmes 
20101029 
tuned

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 
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 
20100917 
boehmes 
20100917 
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions

file  diff  annotate 
20100828 
haftmann 
20100828 
formerly unnamed infix equality now named HOL.eq

file  diff  annotate 
20100713 
boehmes 
20100713 
fixed handling of Ball/Bex: turn equalities into metaequalities for the rewriting conversions;
added tests for Ball/Bex

file  diff  annotate 
20100527 
boehmes 
20100527 
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")

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 