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

2014-06-12 blanchet [Thu, 12 Jun 2014 01:00:49 +0200] rev 57225
register record extensions as freely generated types
src/HOL/Random.thy src/HOL/Tools/record.ML

2014-06-11 haftmann [Wed, 11 Jun 2014 18:22:05 +0200] rev 57224
mixin definitions are within scope of "for"s of import expression
src/Tools/permanent_interpretation.ML

2014-06-11 haftmann [Wed, 11 Jun 2014 18:22:04 +0200] rev 57223
proper proof context transfer wrt. background theory avoids ad-hoc restore operation
src/Tools/permanent_interpretation.ML

2014-06-11 blanchet [Wed, 11 Jun 2014 19:32:39 +0200] rev 57222
refactoring
src/HOL/Tools/SMT2/smtlib2_proof.ML src/HOL/Tools/SMT2/z3_new_real.ML