2014-06-02 blanchet [Mon, 02 Jun 2014 17:34:27 +0200] rev 57159
refactored Z3 to Isar proof construction code
src/HOL/SMT2.thy src/HOL/Tools/SMT2/smt2_solver.ML src/HOL/Tools/SMT2/z3_new_isar.ML src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML

2014-06-02 blanchet [Mon, 02 Jun 2014 17:34:26 +0200] rev 57158
simplified counterexample handling
src/HOL/Tools/SMT2/smt2_failure.ML src/HOL/Tools/SMT2/smt2_solver.ML src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML

2014-06-02 blanchet [Mon, 02 Jun 2014 17:34:26 +0200] rev 57157
split replay and proof parsing for Z3
src/HOL/SMT2.thy src/HOL/Tools/SMT2/smt2_config.ML src/HOL/Tools/SMT2/smt2_solver.ML src/HOL/Tools/SMT2/smt2_systems.ML src/HOL/Tools/SMT2/z3_new_replay.ML

2014-06-02 blanchet [Mon, 02 Jun 2014 17:34:25 +0200] rev 57156
removed counterexample parser (obsolete and useless in practice)
src/HOL/SMT2.thy src/HOL/Tools/SMT2/smt2_solver.ML src/HOL/Tools/SMT2/smt2_systems.ML src/HOL/Tools/SMT2/z3_new_model.ML

2014-06-02 hoelzl [Mon, 02 Jun 2014 16:19:37 +0200] rev 57155
remove superfluous assumption
src/HOL/NthRoot.thy

2014-06-02 fleury [Mon, 02 Jun 2014 15:10:18 +0200] rev 57154
basic setup for zipperposition prover
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML src/HOL/TPTP/atp_problem_import.ML src/HOL/Tools/ATP/atp_proof.ML src/HOL/Tools/ATP/atp_systems.ML src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

2014-06-02 desharna [Mon, 02 Jun 2014 14:29:20 +0200] rev 57153
document property 'sel_set'
src/Doc/Datatypes/Datatypes.thy

2014-06-02 desharna [Mon, 02 Jun 2014 14:29:20 +0200] rev 57152
generate 'sel_set' theorem for (co)datatypes
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML

2014-06-02 blanchet [Mon, 02 Jun 2014 11:59:51 +0200] rev 57151
removed some spurious warnings in new (co)datatype package
src/HOL/Tools/BNF/bnf_lfp_size.ML

2014-06-02 blanchet [Mon, 02 Jun 2014 11:59:50 +0200] rev 57150
add option to keep duplicates, for more precise evaluation of relevance filters
src/HOL/TPTP/MaSh_Export.thy src/HOL/TPTP/mash_eval.ML src/HOL/TPTP/mash_export.ML src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML