2005-11-10 wenzelm [Thu, 10 Nov 2005 20:57:21 +0100] rev 18151
guess: Seq.hd;
Term.find_free;
src/Pure/Isar/obtain.ML

2005-11-10 wenzelm [Thu, 10 Nov 2005 20:57:20 +0100] rev 18150
guess: Toplevel.proof;
src/Pure/Isar/isar_syn.ML

2005-11-10 wenzelm [Thu, 10 Nov 2005 20:57:19 +0100] rev 18149
added find_free (from Isar/proof_context.ML);
src/Pure/term.ML

2005-11-10 wenzelm [Thu, 10 Nov 2005 20:57:18 +0100] rev 18148
curried multiply;
src/Pure/library.ML

2005-11-10 wenzelm [Thu, 10 Nov 2005 20:57:17 +0100] rev 18147
induct method: fixes;
tuned;
src/Provers/induct_method.ML

2005-11-10 wenzelm [Thu, 10 Nov 2005 20:57:16 +0100] rev 18146
uncurried Consts.typargs;
src/Provers/blast.ML src/Pure/consts.ML src/Pure/sign.ML

2005-11-10 wenzelm [Thu, 10 Nov 2005 20:57:11 +0100] rev 18145
renamed Thm.cgoal_of to Thm.cprem_of;
NEWS src/HOL/Tools/datatype_aux.ML src/HOL/Tools/record_package.ML src/HOLCF/adm_tac.ML src/Provers/splitter.ML src/Pure/Isar/method.ML src/Pure/goal.ML src/Pure/tactic.ML src/Pure/thm.ML

2005-11-10 paulson [Thu, 10 Nov 2005 17:33:14 +0100] rev 18144
duplicate axioms in ATP linkup, and general fixes
src/HOL/Set.thy src/HOL/Tools/ATP/res_clasimpset.ML src/HOL/Tools/res_axioms.ML

2005-11-10 paulson [Thu, 10 Nov 2005 17:31:44 +0100] rev 18143
tidying
src/HOL/Library/Zorn.thy

2005-11-10 urbanc [Thu, 10 Nov 2005 00:36:26 +0100] rev 18142
called the induction principle "unsafe" instead of "test".
src/HOL/Nominal/nominal_package.ML