2009-09-29 wenzelm [Tue, 29 Sep 2009 11:49:22 +0200] rev 32738
explicit indication of Unsynchronized.ref;
src/Pure/Concurrent/future.ML src/Pure/Concurrent/synchronized.ML src/Pure/Concurrent/synchronized_dummy.ML src/Pure/General/file.ML src/Pure/General/lazy.ML src/Pure/General/markup.ML src/Pure/General/name_space.ML src/Pure/General/output.ML src/Pure/General/pretty.ML src/Pure/General/print_mode.ML src/Pure/General/secure.ML src/Pure/Isar/code.ML src/Pure/Isar/isar_document.ML src/Pure/Isar/local_syntax.ML src/Pure/Isar/method.ML src/Pure/Isar/outer_keyword.ML src/Pure/Isar/outer_lex.ML src/Pure/Isar/outer_syntax.ML src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/toplevel.ML src/Pure/ML-Systems/compiler_polyml-5.0.ML src/Pure/ML-Systems/compiler_polyml-5.2.ML src/Pure/ML-Systems/compiler_polyml-5.3.ML src/Pure/ML-Systems/multithreading_polyml.ML src/Pure/ML/ml_compiler_polyml-5.3.ML src/Pure/ML/ml_context.ML src/Pure/Proof/extraction.ML src/Pure/Proof/reconstruct.ML src/Pure/ProofGeneral/preferences.ML src/Pure/ProofGeneral/proof_general_emacs.ML src/Pure/ProofGeneral/proof_general_pgip.ML src/Pure/ROOT.ML src/Pure/Syntax/ast.ML src/Pure/Syntax/parser.ML src/Pure/Syntax/printer.ML src/Pure/Syntax/syn_trans.ML src/Pure/Syntax/syntax.ML src/Pure/System/isabelle_process.ML src/Pure/System/isar.ML src/Pure/System/session.ML src/Pure/Thy/html.ML src/Pure/Thy/present.ML src/Pure/Thy/thy_info.ML src/Pure/Thy/thy_load.ML src/Pure/Thy/thy_output.ML src/Pure/Tools/find_theorems.ML src/Pure/codegen.ML src/Pure/context.ML src/Pure/display.ML ...

2009-09-29 wenzelm [Tue, 29 Sep 2009 11:48:32 +0200] rev 32737
Raw ML references as unsynchronized state variables.
src/Pure/IsaMakefile src/Pure/ML-Systems/mosml.ML src/Pure/ML-Systems/polyml_common.ML src/Pure/ML-Systems/smlnj.ML src/Pure/ML-Systems/unsynchronized.ML src/Pure/library.ML

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