2006-09-19 haftmann [Tue, 19 Sep 2006 15:22:03 +0200] rev 20596
(void)
src/HOL/Integ/Numeral.thy src/Pure/Pure.thy src/Pure/Tools/nbe_eval.ML

2006-09-19 haftmann [Tue, 19 Sep 2006 15:21:58 +0200] rev 20595
improved numeral handling for nbe
src/HOL/Integ/IntArith.thy src/HOL/Integ/IntDef.thy src/HOL/Integ/NatBin.thy src/HOL/Integ/Presburger.thy src/HOL/Presburger.thy src/HOL/ex/NormalForm.thy src/HOL/ex/reflection.ML

2006-09-19 haftmann [Tue, 19 Sep 2006 15:21:55 +0200] rev 20594
added suspensions in Pure
src/HOL/Import/ImportRecorder.thy src/HOL/Import/lazy_seq.ML src/HOL/Import/susp.ML src/Pure/General/ROOT.ML src/Pure/General/susp.ML

2006-09-19 haftmann [Tue, 19 Sep 2006 15:21:52 +0200] rev 20593
added some stuff for code generation 2
src/HOL/Extraction/Higman.thy src/HOL/Extraction/Pigeonhole.thy src/HOL/Extraction/QuotRem.thy src/HOL/MicroJava/BV/BVExample.thy

2006-09-19 haftmann [Tue, 19 Sep 2006 15:21:51 +0200] rev 20592
dropped error-prone code generation 2 for wfrec
src/HOL/Wellfounded_Recursion.thy

2006-09-19 haftmann [Tue, 19 Sep 2006 15:21:48 +0200] rev 20591
text cleanup
src/HOL/PreList.thy

2006-09-19 haftmann [Tue, 19 Sep 2006 15:21:44 +0200] rev 20590
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
src/HOL/HOL.thy

2006-09-19 haftmann [Tue, 19 Sep 2006 15:21:43 +0200] rev 20589
explicit divmod algorithm for code generation
src/HOL/Divides.thy

2006-09-19 haftmann [Tue, 19 Sep 2006 15:21:42 +0200] rev 20588
added operational equality
src/HOL/Datatype.thy src/HOL/List.thy src/HOL/Nat.thy src/HOL/Orderings.thy src/HOL/Product_Type.thy src/HOL/Sum_Type.thy

2006-09-19 haftmann [Tue, 19 Sep 2006 15:21:41 +0200] rev 20587
added section on code generation 2
doc-src/IsarRef/logics.tex