2008-10-28 ballarin [Tue, 28 Oct 2008 17:53:46 +0100] rev 28707
Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
src/Pure/Isar/theory_target.ML

2008-10-28 haftmann [Tue, 28 Oct 2008 16:59:02 +0100] rev 28706
restored incremental code generation
src/Tools/code/code_thingol.ML src/Tools/nbe.ML

2008-10-28 haftmann [Tue, 28 Oct 2008 16:59:01 +0100] rev 28705
slightly tuned
src/Tools/code/code_ml.ML

2008-10-28 haftmann [Tue, 28 Oct 2008 16:59:00 +0100] rev 28704
assert that no class parameter is used as constructor
src/Pure/Isar/code_unit.ML

2008-10-28 haftmann [Tue, 28 Oct 2008 16:58:59 +0100] rev 28703
cleanup code default attribute
src/HOL/Tools/datatype_package.ML src/HOL/Tools/function_package/fundef_package.ML src/HOL/Tools/old_primrec_package.ML src/HOL/Tools/primrec_package.ML src/HOL/Tools/recdef_package.ML src/HOL/Tools/recfun_codegen.ML src/Pure/Isar/code.ML src/Pure/Isar/specification.ML

2008-10-28 haftmann [Tue, 28 Oct 2008 12:29:57 +0100] rev 28702
removed includes
src/HOL/Library/Coinductive_List.thy

2008-10-28 haftmann [Tue, 28 Oct 2008 12:28:14 +0100] rev 28701
making SMLNJ happy
src/Pure/Isar/expression.ML

2008-10-28 paulson [Tue, 28 Oct 2008 11:05:44 +0100] rev 28700
The metis method no longer fails because the theorem is too trivial
NEWS src/HOL/Tools/metis_tools.ML

2008-10-28 ballarin [Tue, 28 Oct 2008 11:03:07 +0100] rev 28699
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
src/FOL/FOL.thy src/FOL/IFOL.thy src/HOL/Code_Setup.thy src/HOL/Groebner_Basis.thy src/HOL/HOL.thy src/HOL/Library/Dense_Linear_Order.thy src/Pure/Pure.thy

2008-10-27 paulson [Mon, 27 Oct 2008 18:14:34 +0100] rev 28698
metis proof
src/HOL/Auth/Message.thy