2006-11-22 haftmann [Wed, 22 Nov 2006 10:20:19 +0100] rev 21459
no explicit check for theory Nat
src/HOL/Tools/datatype_package.ML

2006-11-22 haftmann [Wed, 22 Nov 2006 10:20:18 +0100] rev 21458
added code lemmas
src/HOL/Library/List_lexord.thy src/HOL/Library/Product_ord.thy

2006-11-22 haftmann [Wed, 22 Nov 2006 10:20:17 +0100] rev 21457
does not import Hilber_Choice any longer
src/HOL/PreList.thy

2006-11-22 haftmann [Wed, 22 Nov 2006 10:20:16 +0100] rev 21456
cleanup
src/HOL/Nat.thy src/HOL/Power.thy

2006-11-22 haftmann [Wed, 22 Nov 2006 10:20:15 +0100] rev 21455
incorporated structure HOList into HOLogic
src/HOL/Library/MLString.thy src/HOL/List.thy src/HOL/ex/CodeEmbed.thy src/HOL/hologic.ML

2006-11-22 haftmann [Wed, 22 Nov 2006 10:20:12 +0100] rev 21454
dropped eq const
src/HOL/Code_Generator.thy src/HOL/Datatype.thy src/HOL/Integ/IntDef.thy src/HOL/Integ/Presburger.thy src/HOL/Library/EfficientNat.thy src/HOL/Library/ExecutableRat.thy src/HOL/Library/ExecutableSet.thy src/HOL/Presburger.thy src/HOL/Product_Type.thy src/HOL/Sum_Type.thy src/HOL/Tools/datatype_codegen.ML

2006-11-22 haftmann [Wed, 22 Nov 2006 10:20:11 +0100] rev 21453
removed Extraction dependency
src/HOL/ATP_Linkup.thy

2006-11-22 haftmann [Wed, 22 Nov 2006 10:20:09 +0100] rev 21452
final draft
doc-src/IsarAdvanced/Codegen/Makefile doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML doc-src/IsarAdvanced/Codegen/codegen_process.pdf doc-src/IsarAdvanced/Codegen/codegen_process.ps

2006-11-21 wenzelm [Tue, 21 Nov 2006 20:58:15 +0100] rev 21451
made SML/NJ happy;
src/Pure/Isar/proof.ML

2006-11-21 wenzelm [Tue, 21 Nov 2006 20:48:11 +0100] rev 21450
theorem(_i): note assms of statement;
src/Pure/Isar/specification.ML