2014-06-12 hoelzl [Thu, 12 Jun 2014 15:47:36 +0200] rev 57235
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
CONTRIBUTORS src/HOL/Probability/Binary_Product_Measure.thy src/HOL/Probability/Bochner_Integration.thy src/HOL/Probability/Borel_Space.thy src/HOL/Probability/Convolution.thy src/HOL/Probability/Distributions.thy src/HOL/Probability/Independent_Family.thy src/HOL/Probability/Information.thy src/HOL/Probability/Lebesgue_Measure.thy src/HOL/Probability/Measure_Space.thy src/HOL/Probability/Probability_Measure.thy

2014-06-11 hoelzl [Wed, 11 Jun 2014 13:39:38 +0200] rev 57234
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
src/HOL/Library/ContNotDenum.thy src/HOL/Library/Countable_Set.thy

2014-06-12 haftmann [Thu, 12 Jun 2014 08:48:59 +0200] rev 57233
uniform treatment of trivial unit instances: simplify by default, unfold in code preprocessor
src/HOL/Product_Type.thy

2014-06-12 blanchet [Thu, 12 Jun 2014 01:00:49 +0200] rev 57232
adapted examples to changes in SMT triggers
src/HOL/SMT_Examples/SMT_Examples.thy src/HOL/SMT_Examples/SMT_Tests.thy src/HOL/SMT_Examples/VCC_Max.certs2 src/HOL/SMT_Examples/boogie.ML

2014-06-12 blanchet [Thu, 12 Jun 2014 01:00:49 +0200] rev 57231
reduces Sledgehammer dependencies
src/HOL/List.thy src/HOL/Nitpick.thy src/HOL/SMT.thy src/HOL/Sledgehammer.thy

2014-06-12 blanchet [Thu, 12 Jun 2014 01:00:49 +0200] rev 57230
eliminate dependency of SMT2 module on 'list'
src/HOL/SMT2.thy src/HOL/Tools/SMT2/smt2_builtin.ML src/HOL/Tools/SMT2/smt2_config.ML src/HOL/Tools/SMT2/smt2_normalize.ML src/HOL/Tools/SMT2/smt2_translate.ML src/HOL/Tools/SMT2/smt2_util.ML src/HOL/Tools/SMT2/smtlib2_proof.ML src/HOL/Tools/SMT2/z3_new_replay.ML src/HOL/Tools/SMT2/z3_new_replay_literals.ML src/HOL/Tools/SMT2/z3_new_replay_methods.ML src/HOL/Tools/SMT2/z3_new_replay_rules.ML src/HOL/Tools/SMT2/z3_new_replay_util.ML

2014-06-12 blanchet [Thu, 12 Jun 2014 01:00:49 +0200] rev 57229
tuning
src/HOL/SMT.thy src/HOL/Tools/SMT2/smt2_builtin.ML src/HOL/Tools/SMT2/smt2_config.ML src/HOL/Tools/SMT2/smt2_datatypes.ML src/HOL/Tools/SMT2/smt2_failure.ML src/HOL/Tools/SMT2/smt2_normalize.ML src/HOL/Tools/SMT2/smt2_real.ML src/HOL/Tools/SMT2/smt2_solver.ML src/HOL/Tools/SMT2/smt2_systems.ML src/HOL/Tools/SMT2/smt2_translate.ML src/HOL/Tools/SMT2/smt2_util.ML src/HOL/Tools/SMT2/smtlib2.ML src/HOL/Tools/SMT2/smtlib2_interface.ML src/HOL/Tools/SMT2/z3_new_interface.ML src/HOL/Tools/SMT2/z3_new_proof.ML src/HOL/Tools/SMT2/z3_new_real.ML src/HOL/Tools/SMT2/z3_new_replay.ML src/HOL/Tools/SMT2/z3_new_replay_literals.ML src/HOL/Tools/SMT2/z3_new_replay_methods.ML src/HOL/Tools/SMT2/z3_new_replay_rules.ML src/HOL/Tools/SMT2/z3_new_replay_util.ML src/HOL/Word/Tools/smt2_word.ML

2014-06-12 blanchet [Thu, 12 Jun 2014 01:00:49 +0200] rev 57228
removed subsumed record-related code, now that records are registered as 'ctr_sugar'
src/HOL/Tools/Nitpick/nitpick_hol.ML

2014-06-12 blanchet [Thu, 12 Jun 2014 01:00:49 +0200] rev 57227
made lookup more robust in the face of missing (dummy) case constant
src/HOL/Tools/Nitpick/nitpick_hol.ML

2014-06-12 blanchet [Thu, 12 Jun 2014 01:00:49 +0200] rev 57226
use 'ctr_sugar' abstraction in SMT(2)
src/HOL/SMT.thy src/HOL/SMT2.thy src/HOL/Tools/SMT/smt_datatypes.ML src/HOL/Tools/SMT2/smt2_datatypes.ML