2013-10-01 blanchet [Tue, 01 Oct 2013 14:05:25 +0200] rev 54006
renamed theory file
src/HOL/BNF/BNF_Ctr_Sugar.thy src/HOL/BNF/BNF_FP_Base.thy src/HOL/BNF/Ctr_Sugar.thy src/HOL/BNF/Tools/bnf_ctr_sugar.ML src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML src/HOL/BNF/Tools/bnf_fp_def_sugar.ML src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML src/HOL/BNF/Tools/bnf_lfp_compat.ML

2013-10-01 wenzelm [Tue, 01 Oct 2013 12:53:24 +0200] rev 54005
tuned signature -- facilitate experimentation with other processes;
src/Pure/System/isabelle_process.scala src/Pure/System/system_channel.scala

2013-09-30 Christian Sternagel [Mon, 30 Sep 2013 22:01:46 +0900] rev 54004
preserve types during rewriting
src/Tools/adhoc_overloading.ML

2013-09-30 blanchet [Mon, 30 Sep 2013 22:36:43 +0200] rev 54003
made SML/NJ happy
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML src/HOL/BNF/Tools/bnf_lfp_compat.ML

2013-09-30 blanchet [Mon, 30 Sep 2013 18:08:35 +0200] rev 54002
made SML/NJ happy
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

2013-09-30 blanchet [Mon, 30 Sep 2013 17:53:44 +0200] rev 54001
made SML/NJ happier
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

2013-09-30 blanchet [Mon, 30 Sep 2013 17:47:50 +0200] rev 54000
added experimental configuration options to tune use of builtin symbols in SMT
src/HOL/Tools/SMT/smt_builtin.ML src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

2013-09-30 blanchet [Mon, 30 Sep 2013 16:28:54 +0200] rev 53999
added possibility to reset builtins (for experimentation)
src/HOL/Tools/SMT/smt_builtin.ML

2013-09-30 blanchet [Mon, 30 Sep 2013 16:07:56 +0200] rev 53998
just one data slot (record) per program unit
src/HOL/Tools/SMT/smt_builtin.ML

2013-09-30 blanchet [Mon, 30 Sep 2013 15:10:18 +0200] rev 53997
more "primrec_new" documentation
src/Doc/Datatypes/Datatypes.thy