2007-09-25 wenzelm [Tue, 25 Sep 2007 15:34:35 +0200] rev 24711
simplified interpretation setup;
src/HOL/Tools/datatype_codegen.ML src/HOL/Tools/datatype_package.ML src/HOL/Tools/datatype_realizer.ML src/HOL/Tools/function_package/fundef_package.ML src/HOL/Tools/function_package/size.ML src/HOL/Tools/typecopy_package.ML src/Pure/interpretation.ML

2007-09-25 haftmann [Tue, 25 Sep 2007 13:42:59 +0200] rev 24710
size hook
src/HOL/Tools/function_package/size.ML

2007-09-25 wenzelm [Tue, 25 Sep 2007 13:28:42 +0200] rev 24709
removed redundant global_parse operations;
renamed global_XXX to XXX_global;
src/Pure/Syntax/syntax.ML

2007-09-25 wenzelm [Tue, 25 Sep 2007 13:28:41 +0200] rev 24708
Syntax.parse/check/read;
no export of read/cert_axm;
src/Pure/theory.ML

2007-09-25 wenzelm [Tue, 25 Sep 2007 13:28:37 +0200] rev 24707
Syntax.parse/check/read;
src/FOLP/simp.ML src/HOL/Import/import_syntax.ML src/HOL/Import/proof_kernel.ML src/HOL/Nominal/nominal_primrec.ML src/HOL/Tools/TFL/post.ML src/HOL/Tools/primrec_package.ML src/HOL/Tools/specification_package.ML src/HOLCF/IOA/meta_theory/ioa_package.ML src/HOLCF/Tools/cont_consts.ML src/HOLCF/Tools/domain/domain_extender.ML src/HOLCF/Tools/fixrec_package.ML src/Provers/splitter.ML src/Pure/Isar/class.ML src/Pure/Isar/code_unit.ML src/Pure/Proof/extraction.ML src/Pure/codegen.ML src/Pure/meta_simplifier.ML src/Pure/sign.ML src/ZF/Tools/datatype_package.ML src/ZF/Tools/primrec_package.ML

2007-09-25 wenzelm [Tue, 25 Sep 2007 13:28:35 +0200] rev 24706
* Pure/Syntax: generic interfaces for parsing and type checking;
tuned;
NEWS

2007-09-25 ballarin [Tue, 25 Sep 2007 12:59:24 +0200] rev 24705
Simplified proof due to improved integration of order_tac and simp.
src/HOL/List.thy

2007-09-25 ballarin [Tue, 25 Sep 2007 12:56:27 +0200] rev 24704
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
src/HOL/Orderings.thy src/Provers/order.ML

2007-09-25 haftmann [Tue, 25 Sep 2007 12:16:15 +0200] rev 24703
dropped
src/Pure/Tools/nbe.ML src/Pure/Tools/nbe_codegen.ML src/Pure/Tools/nbe_eval.ML

2007-09-25 haftmann [Tue, 25 Sep 2007 12:16:14 +0200] rev 24702
ML monad support
src/Tools/code/code_target.ML