2007-10-04 wenzelm [Thu, 04 Oct 2007 16:59:30 +0200] rev 24834
abs_conv/forall_conv: proper context (avoid gensym);
removed unused cache_conv;
src/Pure/conv.ML

2007-10-04 wenzelm [Thu, 04 Oct 2007 16:59:29 +0200] rev 24833
load variable.ML before conv.ML;
src/Pure/ROOT.ML

2007-10-04 wenzelm [Thu, 04 Oct 2007 16:59:28 +0200] rev 24832
Conv.forall_conv: proper context;
src/HOL/Nominal/nominal_inductive.ML src/Pure/Isar/object_logic.ML src/Tools/induct.ML

2007-10-04 wenzelm [Thu, 04 Oct 2007 16:21:31 +0200] rev 24831
cover AFP logs as well, using "afp" pseudo-platform;
Admin/isatest/isatest-statistics Admin/isatest/isatest-stats

2007-10-04 wenzelm [Thu, 04 Oct 2007 14:42:47 +0200] rev 24830
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
src/FOL/FOL.thy src/FOL/IFOL.thy src/FOL/IsaMakefile src/HOL/HOL.thy src/HOL/IsaMakefile src/HOL/Nominal/nominal_induct.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Tools/datatype_package.ML src/HOL/Tools/function_package/fundef_package.ML src/HOL/Tools/inductive_package.ML src/HOL/Tools/record_package.ML src/HOL/Tools/typedef_package.ML src/Provers/induct_method.ML src/Pure/IsaMakefile src/Pure/Isar/ROOT.ML src/Pure/Isar/induct_attrib.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML src/Tools/induct.ML src/ZF/Tools/inductive_package.ML

2007-10-04 wenzelm [Thu, 04 Oct 2007 14:42:11 +0200] rev 24829
avoid gensym;
src/Pure/Thy/present.ML

2007-10-04 wenzelm [Thu, 04 Oct 2007 13:26:34 +0200] rev 24828
updated Sign.add_abbrev;
doc-src/IsarImplementation/Thy/document/logic.tex doc-src/IsarImplementation/Thy/logic.thy

2007-10-04 paulson [Thu, 04 Oct 2007 12:32:58 +0200] rev 24827
combinator translation
src/HOL/ATP_Linkup.thy src/HOL/MetisExamples/Abstraction.thy src/HOL/MetisExamples/Tarski.thy src/HOL/Tools/meson.ML src/HOL/Tools/metis_tools.ML src/HOL/Tools/res_atp.ML src/HOL/Tools/res_axioms.ML

2007-10-03 wenzelm [Wed, 03 Oct 2007 22:33:17 +0200] rev 24826
avoid unnamed infixes;
src/ZF/Inductive.thy src/ZF/OrderType.thy src/ZF/Tools/datatype_package.ML src/ZF/Tools/induct_tacs.ML src/ZF/Tools/inductive_package.ML src/ZF/Tools/typechk.ML src/ZF/ZF.thy src/ZF/ind_syntax.ML src/ZF/simpdata.ML

2007-10-03 wenzelm [Wed, 03 Oct 2007 21:29:05 +0200] rev 24825
avoid unnamed infixes;
tuned;
src/CCL/CCL.thy src/CCL/Fix.thy src/CCL/Set.thy src/CCL/Term.thy src/CCL/Trancl.thy src/CCL/Type.thy src/CCL/Wfd.thy src/CCL/ex/List.thy src/CCL/ex/Nat.thy