2010-12-07 boehmes [Tue, 07 Dec 2010 15:55:35 +0100] rev 41065
merged
src/HOL/IsaMakefile src/HOL/Probability/Positive_Infinite_Real.thy src/HOL/Tools/SMT/smt_solver.ML src/HOL/Tools/async_manager.ML

2010-12-07 boehmes [Tue, 07 Dec 2010 15:44:38 +0100] rev 41064
updated SMT certificates
src/HOL/Boogie/Examples/Boogie_Dijkstra.certs src/HOL/Boogie/Examples/Boogie_Max.certs src/HOL/Boogie/Examples/VCC_Max.certs src/HOL/Multivariate_Analysis/Integration.certs src/HOL/SMT_Examples/SMT_Examples.certs src/HOL/SMT_Examples/SMT_Tests.certs src/HOL/SMT_Examples/SMT_Word_Examples.certs

2010-12-07 boehmes [Tue, 07 Dec 2010 15:01:42 +0100] rev 41063
reduced unnecessary complexity; improved documentation; tuned
src/HOL/Tools/SMT/smt_monomorph.ML

2010-12-07 boehmes [Tue, 07 Dec 2010 15:01:37 +0100] rev 41062
tuned
src/HOL/Tools/SMT/smt_solver.ML

2010-12-07 boehmes [Tue, 07 Dec 2010 14:54:31 +0100] rev 41061
centralized handling of built-in types and constants for bitvectors
src/HOL/Word/Tools/smt_word.ML

2010-12-07 boehmes [Tue, 07 Dec 2010 14:53:44 +0100] rev 41060
moved smt_word.ML into the directory of the Word library
src/HOL/IsaMakefile src/HOL/Tools/SMT/smt_word.ML src/HOL/Word/Tools/smt_word.ML src/HOL/Word/Word.thy

2010-12-07 boehmes [Tue, 07 Dec 2010 14:53:12 +0100] rev 41059
centralized handling of built-in 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 built-in symbols);
removed term_eq in favor of type replacements: term-level occurrences of type bool are replaced by type term_bool (only for the translation)
src/HOL/SMT.thy src/HOL/Tools/SMT/smt_builtin.ML src/HOL/Tools/SMT/smt_config.ML src/HOL/Tools/SMT/smt_normalize.ML src/HOL/Tools/SMT/smt_real.ML src/HOL/Tools/SMT/smt_solver.ML src/HOL/Tools/SMT/smt_translate.ML src/HOL/Tools/SMT/smtlib_interface.ML src/HOL/Tools/SMT/z3_interface.ML src/HOL/Tools/Sledgehammer/sledgehammer.ML

2010-12-06 boehmes [Mon, 06 Dec 2010 16:54:22 +0100] rev 41058
more aggressive unfolding of unknowns in Z3 models
src/HOL/Tools/SMT/z3_model.ML

2010-12-06 boehmes [Mon, 06 Dec 2010 15:38:02 +0100] rev 41057
tuned
src/HOL/Tools/SMT/smt_translate.ML src/HOL/Tools/SMT/smtlib_interface.ML

2010-12-07 bulwahn [Tue, 07 Dec 2010 13:33:28 +0100] rev 41056
adding a definition for refl_on which is friendly for quickcheck and nitpick
src/HOL/Relation.thy