2009-10-29 wenzelm [Thu, 29 Oct 2009 23:56:33 +0100] rev 33339
eliminated some old folds;
src/FOLP/simp.ML src/HOL/Import/lazy_seq.ML src/HOL/Import/proof_kernel.ML src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML src/HOL/Tools/Function/size.ML src/HOL/Tools/TFL/post.ML src/HOL/Tools/TFL/rules.ML src/HOL/Tools/TFL/tfl.ML src/HOL/Tools/choice_specification.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/meson.ML src/HOL/Tools/metis_tools.ML src/HOL/Tools/refute.ML src/HOL/Tools/res_axioms.ML src/HOL/Tools/simpdata.ML src/Provers/classical.ML src/Provers/typedsimp.ML src/ZF/Tools/datatype_package.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 23:49:55 +0100] rev 33338
eliminated some old folds;
src/HOL/Nominal/nominal_datatype.ML src/HOL/Tools/Datatype/datatype_abs_proofs.ML src/HOL/Tools/Datatype/datatype_aux.ML src/HOL/Tools/Datatype/datatype_prop.ML src/HOL/Tools/Datatype/datatype_realizer.ML src/HOL/Tools/Datatype/datatype_rep_proofs.ML src/HOL/Tools/inductive.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/old_primrec.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 23:48:56 +0100] rev 33337
eliminated some old folds;
src/Pure/Proof/extraction.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 20:53:24 +0100] rev 33336
less aggressive tracing;
src/Pure/meta_simplifier.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 20:35:47 +0100] rev 33335
DEEPEN: less aggressive tracing, subject to trace_DEEPEN;
src/Pure/search.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 18:53:58 +0100] rev 33334
merged
src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML src/HOL/ex/predicate_compile.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 18:17:26 +0100] rev 33333
merged
src/HOL/IsaMakefile src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

2009-10-29 bulwahn [Thu, 29 Oct 2009 14:06:49 +0100] rev 33332
removing ancient predicate compiler files
src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML src/HOL/ex/predicate_compile.ML

2009-10-29 bulwahn [Thu, 29 Oct 2009 14:03:55 +0100] rev 33331
merged

2009-10-29 bulwahn [Thu, 29 Oct 2009 13:59:37 +0100] rev 33330
encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy
src/HOL/Tools/Predicate_Compile/predicate_compile.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML