2009-11-02 wenzelm [Mon, 02 Nov 2009 20:50:48 +0100] rev 33388
modernized structure Proof_Syntax;
src/HOL/Tools/rewrite_hol_proof.ML src/Pure/Isar/isar_cmd.ML src/Pure/Proof/extraction.ML src/Pure/Proof/proof_syntax.ML src/Pure/Thy/thy_output.ML

2009-11-02 wenzelm [Mon, 02 Nov 2009 20:48:08 +0100] rev 33387
modernized structure Local_Syntax;
src/Pure/Isar/local_syntax.ML src/Pure/Isar/proof_context.ML

2009-11-02 wenzelm [Mon, 02 Nov 2009 20:45:23 +0100] rev 33386
modernized structure AutoBind;
src/Pure/Isar/auto_bind.ML src/Pure/Isar/obtain.ML src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/specification.ML

2009-11-02 wenzelm [Mon, 02 Nov 2009 20:38:46 +0100] rev 33385
modernized structure Primitive_Defs;
src/HOL/Tools/record.ML src/HOL/Tools/typedef.ML src/Pure/Isar/local_defs.ML src/Pure/primitive_defs.ML src/Pure/sign.ML src/ZF/Tools/datatype_package.ML src/ZF/Tools/inductive_package.ML

2009-11-02 wenzelm [Mon, 02 Nov 2009 20:34:59 +0100] rev 33384
modernized structure Simple_Syntax;
src/HOL/Library/OptionalSugar.thy src/HOL/Typerep.thy src/Pure/Syntax/simple_syntax.ML src/Pure/conjunction.ML src/Pure/drule.ML src/Pure/pure_thy.ML

2009-11-02 wenzelm [Mon, 02 Nov 2009 20:30:40 +0100] rev 33383
modernized structure Context_Position;
src/Pure/Isar/local_theory.ML src/Pure/Isar/proof_context.ML src/Pure/context_position.ML

2009-11-02 wenzelm [Mon, 02 Nov 2009 19:56:06 +0100] rev 33382
observe usual naming conventions;
src/Pure/Tools/find_theorems.ML

2009-11-02 krauss [Mon, 02 Nov 2009 16:44:18 +0100] rev 33381
find_theorems: respect conceal flag
src/Pure/Tools/find_theorems.ML

2009-11-02 wenzelm [Mon, 02 Nov 2009 17:30:38 +0100] rev 33380
DEEPEN: all tracing is subject to trace_DEEPEN (NB: Proof General tends to "popup" tracing output);
src/Pure/search.ML

2009-11-02 wenzelm [Mon, 02 Nov 2009 17:29:48 +0100] rev 33379
back to warning -- Proof General tends to "popup" tracing output;
src/Pure/meta_simplifier.ML