2006-02-06 wenzelm [Mon, 06 Feb 2006 20:59:04 +0100] rev 18937
added (beta_)eta_contract (from pattern.ML);
added expand_atom;
src/Pure/envir.ML

2006-02-06 wenzelm [Mon, 06 Feb 2006 20:59:03 +0100] rev 18936
print_theory: const abbreviations;
src/Pure/display.ML

2006-02-06 wenzelm [Mon, 06 Feb 2006 20:59:02 +0100] rev 18935
added abbreviations;
added certify (mostly from sign.ML);
src/Pure/consts.ML

2006-02-06 wenzelm [Mon, 06 Feb 2006 20:59:01 +0100] rev 18934
load envir.ML and logic.ML early;
src/Pure/ROOT.ML

2006-02-06 wenzelm [Mon, 06 Feb 2006 20:59:00 +0100] rev 18933
Logic.rlist_abs;
src/Provers/induct_method.ML

2006-02-06 wenzelm [Mon, 06 Feb 2006 20:58:59 +0100] rev 18932
Logic.const_of_class/class_of_const;
src/HOL/Tools/refute.ML src/Pure/axclass.ML

2006-02-06 wenzelm [Mon, 06 Feb 2006 20:58:57 +0100] rev 18931
TableFun: renamed xxx_multi to xxx_list;
src/HOL/Tools/recfun_codegen.ML src/HOL/Tools/record_package.ML src/Pure/Syntax/syntax.ML src/Pure/Thy/thm_database.ML src/Pure/context.ML src/Pure/fact_index.ML src/Pure/sorts.ML

2006-02-06 wenzelm [Mon, 06 Feb 2006 20:58:56 +0100] rev 18930
replaced Symtab.merge_multi by local merge_rules;
src/HOL/Tools/inductive_codegen.ML

2006-02-06 wenzelm [Mon, 06 Feb 2006 20:58:54 +0100] rev 18929
Envir.(beta_)eta_contract;
src/HOL/Import/proof_kernel.ML src/HOL/Tools/datatype_realizer.ML src/HOL/Tools/inductive_realizer.ML src/Pure/Proof/reconstruct.ML src/Pure/drule.ML src/Pure/meta_simplifier.ML

2006-02-06 haftmann [Mon, 06 Feb 2006 11:01:28 +0100] rev 18928
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
src/HOL/Tools/datatype_package.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/primrec_package.ML src/HOL/Tools/record_package.ML src/HOL/Tools/typedef_package.ML src/HOLCF/domain/extender.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/session.ML src/Pure/Proof/extraction.ML src/Pure/proofterm.ML src/Pure/sign.ML src/Pure/type.ML src/ZF/Tools/primrec_package.ML