2007-09-18 haftmann [Tue, 18 Sep 2007 07:46:00 +0200] rev 24626
introduced generic concepts for theory interpretators
src/HOL/Inductive.thy src/HOL/IsaMakefile src/HOL/Library/Eval.thy src/HOL/Library/Library.thy src/HOL/Tools/datatype_codegen.ML src/HOL/Tools/datatype_hooks.ML src/HOL/Tools/datatype_package.ML src/HOL/Tools/function_package/fundef_package.ML src/HOL/Tools/typecopy_package.ML src/HOL/ex/ExecutableContent.thy src/Pure/theory.ML

2007-09-18 haftmann [Tue, 18 Sep 2007 07:36:38 +0200] rev 24625
separated code for inductive sequences from inductive_codegen.ML
src/HOL/Inductive.thy src/HOL/IsaMakefile src/HOL/Tools/dseq.ML src/HOL/Tools/inductive_codegen.ML

2007-09-18 haftmann [Tue, 18 Sep 2007 07:36:15 +0200] rev 24624
distinction between regular and default code theorems
src/HOL/Tools/datatype_codegen.ML src/HOL/Tools/datatype_package.ML src/HOL/Tools/function_package/fundef_package.ML src/HOL/Tools/primrec_package.ML src/HOL/Tools/recdef_package.ML src/HOL/Tools/recfun_codegen.ML src/HOL/Tools/record_package.ML src/HOL/Tools/typecopy_package.ML src/Pure/Isar/code.ML src/Pure/Isar/code_unit.ML src/Pure/Isar/constdefs.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/specification.ML src/Pure/Proof/extraction.ML

2007-09-18 haftmann [Tue, 18 Sep 2007 07:36:14 +0200] rev 24623
renamed constructor RealC to Ratreal
src/HOL/Real/RealDef.thy

2007-09-18 haftmann [Tue, 18 Sep 2007 07:36:13 +0200] rev 24622
renamed constructor RatC to Rational
src/HOL/Real/Rational.thy

2007-09-18 haftmann [Tue, 18 Sep 2007 07:36:12 +0200] rev 24621
clarified evaluation code
src/HOL/Library/Eval.thy src/Tools/code/code_package.ML src/Tools/code/code_target.ML

2007-09-18 haftmann [Tue, 18 Sep 2007 07:36:11 +0200] rev 24620
adjusted
lib/Tools/codegen

2007-09-18 haftmann [Tue, 18 Sep 2007 07:36:10 +0200] rev 24619
clarified remark
Admin/CHECKLIST

2007-09-18 haftmann [Tue, 18 Sep 2007 07:36:09 +0200] rev 24618
added script checking for consistency of ML file header
Admin/check_ml_headers

2007-09-18 nipkow [Tue, 18 Sep 2007 07:22:42 +0200] rev 24617
sorting
src/HOL/List.thy