2009-09-28 wenzelm [Mon, 28 Sep 2009 23:51:13 +0200] rev 32736
Dummy version of state variables -- plain refs for sequential access.
src/Pure/Concurrent/synchronized_dummy.ML src/Pure/IsaMakefile src/Pure/ML-Systems/thread_dummy.ML src/Pure/ROOT.ML

2009-09-28 wenzelm [Mon, 28 Sep 2009 23:19:50 +0200] rev 32735
reactivated at-sml-dev-e;
Admin/isatest/isatest-makedist

2009-09-28 wenzelm [Mon, 28 Sep 2009 23:13:37 +0200] rev 32734
misc tuning and modernization;
src/HOL/HOL.thy src/HOL/ex/Coherent.thy src/Tools/coherent.ML

2009-09-28 wenzelm [Mon, 28 Sep 2009 22:47:34 +0200] rev 32733
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
src/HOL/HOL.thy src/HOL/IsaMakefile src/HOL/Nominal/nominal_permeq.ML src/HOL/Tools/Datatype/datatype_aux.ML src/Tools/cong_tac.ML

2009-09-28 wenzelm [Mon, 28 Sep 2009 21:35:57 +0200] rev 32732
merged

2009-09-28 haftmann [Mon, 28 Sep 2009 15:25:43 +0200] rev 32731
less auxiliary functions
src/HOL/Tools/Datatype/datatype.ML

2009-09-28 haftmann [Mon, 28 Sep 2009 14:54:15 +0200] rev 32730
tuned
src/HOL/Tools/Datatype/datatype.ML

2009-09-28 haftmann [Mon, 28 Sep 2009 14:48:30 +0200] rev 32729
shared code between rep_datatype and datatype
src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Datatype/datatype_abs_proofs.ML

2009-09-28 haftmann [Mon, 28 Sep 2009 10:51:12 +0200] rev 32728
further unification of datatype and rep_datatype
src/HOL/Tools/Datatype/datatype.ML

2009-09-28 haftmann [Mon, 28 Sep 2009 10:20:21 +0200] rev 32727
avoid compound fields in datatype info record
src/HOL/Nominal/nominal_datatype.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Datatype/datatype_aux.ML src/HOL/Tools/Datatype/datatype_realizer.ML src/HOL/Tools/Datatype/datatype_rep_proofs.ML src/HOL/Tools/Function/size.ML src/HOL/Tools/TFL/casesplit.ML src/HOL/Tools/old_primrec.ML