2010-03-03 wenzelm [Wed, 03 Mar 2010 00:33:02 +0100] rev 35431
cleanup type translations;
src/HOL/Bali/AxSem.thy src/HOL/Bali/Basis.thy src/HOL/Bali/Decl.thy src/HOL/Bali/DeclConcepts.thy src/HOL/Bali/Eval.thy src/HOL/Bali/Name.thy src/HOL/Bali/State.thy src/HOL/Bali/Table.thy src/HOL/Bali/Term.thy src/HOL/Bali/Type.thy src/HOL/Bali/Value.thy src/HOL/Bali/WellType.thy src/HOL/IMPP/Hoare.thy src/HOL/Library/Numeral_Type.thy src/HOL/MicroJava/J/Decl.thy src/HOL/NanoJava/AxSem.thy src/HOL/NanoJava/Decl.thy src/HOL/NanoJava/State.thy src/HOLCF/One.thy src/HOLCF/Representable.thy src/HOLCF/Tr.thy

2010-03-03 wenzelm [Wed, 03 Mar 2010 00:32:14 +0100] rev 35430
adapted to authentic syntax -- actual types are verbatim;
src/HOL/Tools/numeral_syntax.ML src/HOL/Tools/record.ML src/HOL/Tools/typedef.ML src/HOL/Typerep.thy src/HOL/ex/Numeral.thy src/Sequents/Sequents.thy

2010-03-03 wenzelm [Wed, 03 Mar 2010 00:28:22 +0100] rev 35429
authentic syntax for classes and type constructors;
read/intern formal entities just after raw parsing, extern just before final pretty printing;
discontinued _class token translation;
moved Local_Syntax.extern_term to Syntax/printer.ML;
misc tuning;
src/Pure/Isar/local_syntax.ML src/Pure/Isar/proof_context.ML src/Pure/ML/ml_antiquote.ML src/Pure/Syntax/printer.ML src/Pure/Syntax/syn_ext.ML src/Pure/Syntax/syn_trans.ML src/Pure/Syntax/syntax.ML src/Pure/Syntax/type_ext.ML src/Pure/pure_thy.ML src/Pure/sign.ML

2010-03-03 wenzelm [Wed, 03 Mar 2010 00:00:44 +0100] rev 35428
more systematic mark/unmark operations;
tuned;
src/Pure/Syntax/lexicon.ML

2010-03-02 wenzelm [Tue, 02 Mar 2010 23:59:54 +0100] rev 35427
proper (type_)notation;
src/HOL/Map.thy src/HOL/Product_Type.thy src/HOL/UNITY/Union.thy src/HOLCF/Cfun.thy src/HOLCF/Sprod.thy src/HOLCF/Ssum.thy src/HOLCF/Up.thy src/HOLCF/ex/Strict_Fun.thy src/ZF/Induct/Comb.thy src/ZF/UNITY/Union.thy

2010-03-02 wenzelm [Tue, 02 Mar 2010 23:56:13 +0100] rev 35426
proper antiquotations;
src/HOLCF/holcf_logic.ML

2010-03-02 wenzelm [Tue, 02 Mar 2010 22:20:19 +0100] rev 35425
standard convention for syntax consts;
src/ZF/List_ZF.thy

2010-03-02 wenzelm [Tue, 02 Mar 2010 22:18:51 +0100] rev 35424
more precise scope of exception handler;
src/Pure/Proof/extraction.ML

2010-03-01 wenzelm [Mon, 01 Mar 2010 21:41:35 +0100] rev 35423
eliminated hard tabs;
doc-src/Locales/Locales/Examples3.thy doc-src/Locales/Locales/document/Examples3.tex src/HOL/Imperative_HOL/Heap_Monad.thy src/HOL/Imperative_HOL/ex/Linked_Lists.thy src/HOL/Library/Transitive_Closure_Table.thy

2010-03-01 wenzelm [Mon, 01 Mar 2010 17:45:19 +0100] rev 35422
tuned final whitespace;
src/HOL/UNITY/WFair.thy src/HOL/ZF/LProd.thy src/HOL/ZF/MainZF.thy