2007-12-07 haftmann [Fri, 07 Dec 2007 15:07:56 +0100] rev 25570
proper treatment of code theorems for primrec
src/HOL/Tools/primrec_package.ML src/HOL/Tools/recfun_codegen.ML

2007-12-07 haftmann [Fri, 07 Dec 2007 15:07:54 +0100] rev 25569
dropped Instance.instantiate
src/HOL/Library/Eval.thy src/HOL/Tools/datatype_codegen.ML src/HOL/Tools/function_package/size.ML src/HOL/Tools/typecopy_package.ML src/Pure/Isar/instance.ML

2007-12-07 krauss [Fri, 07 Dec 2007 10:59:03 +0100] rev 25568
Adding "ex/Induction_Scheme.thy" to tests
src/HOL/IsaMakefile src/HOL/ex/ROOT.ML

2007-12-07 krauss [Fri, 07 Dec 2007 09:42:20 +0100] rev 25567
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
src/HOL/FunDef.thy src/HOL/Tools/function_package/induction_scheme.ML src/HOL/ex/Induction_Scheme.thy

2007-12-07 haftmann [Fri, 07 Dec 2007 08:38:50 +0100] rev 25566
tuned further
src/HOL/Tools/primrec_package.ML

2007-12-06 wenzelm [Thu, 06 Dec 2007 22:07:11 +0100] rev 25565
renamed ML_PID to PID;
src/Pure/Tools/isabelle_process.ML

2007-12-06 nipkow [Thu, 06 Dec 2007 19:58:21 +0100] rev 25564
R&F: added sgn lemma
Prefix: sledge-hammered
src/HOL/Library/List_Prefix.thy src/HOL/Ring_and_Field.thy

2007-12-06 haftmann [Thu, 06 Dec 2007 17:05:44 +0100] rev 25563
temporary code generator work arounds
src/HOL/List.thy src/HOL/Nat.thy

2007-12-06 haftmann [Thu, 06 Dec 2007 16:56:00 +0100] rev 25562
fixed slip
src/HOL/Tools/primrec_package.ML

2007-12-06 haftmann [Thu, 06 Dec 2007 16:38:42 +0100] rev 25561
-authentic primrec
src/HOL/Tools/old_primrec_package.ML