2007-07-16 paulson [Mon, 16 Jul 2007 19:11:37 +0200] rev 23815
tidied
src/HOL/Lambda/Commutation.thy

2007-07-16 paulson [Mon, 16 Jul 2007 17:29:34 +0200] rev 23814
tidied using sledgehammer
src/HOL/NumberTheory/Factorization.thy

2007-07-16 paulson [Mon, 16 Jul 2007 17:13:37 +0200] rev 23813
tidied using sledgehammer
src/HOL/ex/Puzzle.thy

2007-07-16 haftmann [Mon, 16 Jul 2007 09:29:05 +0200] rev 23812
clarified structure names
src/Pure/Tools/codegen_package.ML

2007-07-16 haftmann [Mon, 16 Jul 2007 09:29:04 +0200] rev 23811
added function for case certificates
src/HOL/Tools/datatype_codegen.ML src/HOL/ex/Codegenerator.thy src/HOL/ex/Codegenerator_Rat.thy

2007-07-16 haftmann [Mon, 16 Jul 2007 09:29:03 +0200] rev 23810
dropped outer ROOT structure for generated code
src/HOL/Complex/ex/ReflectedFerrack.thy src/HOL/Extraction/Higman.thy src/HOL/Extraction/Pigeonhole.thy src/HOL/Lambda/WeakNorm.thy src/HOL/ex/Classpackage.thy

2007-07-16 haftmann [Mon, 16 Jul 2007 09:29:02 +0200] rev 23809
tuned
src/HOL/Library/EfficientNat.thy src/Pure/Tools/codegen_serializer.ML

2007-07-16 haftmann [Mon, 16 Jul 2007 09:29:01 +0200] rev 23808
fixed SML/NJ int problem
src/HOL/Complex/ex/linreif.ML src/HOL/ex/ROOT.ML src/HOL/ex/Reflected_Presburger.thy src/HOL/ex/coopereif.ML

2007-07-16 haftmann [Mon, 16 Jul 2007 09:29:00 +0200] rev 23807
updated
doc-src/IsarRef/logics.tex

2007-07-13 wenzelm [Fri, 13 Jul 2007 22:36:10 +0200] rev 23806
tuned;
src/Pure/Isar/proof.ML