2014-08-19 wenzelm [Tue, 19 Aug 2014 17:00:44 +0200] rev 58008
added PARALLEL_ALLGOALS convenience;
NEWS src/Provers/clasimp.ML src/Pure/goal.ML src/Pure/simplifier.ML

2014-08-19 wenzelm [Tue, 19 Aug 2014 16:46:07 +0200] rev 58007
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
src/Pure/Isar/method.ML src/Pure/Isar/proof.ML

2014-08-19 wenzelm [Tue, 19 Aug 2014 16:09:11 +0200] rev 58006
tuned signature;
src/Pure/Isar/method.ML

2014-08-19 wenzelm [Tue, 19 Aug 2014 15:55:06 +0200] rev 58005
more compact datatypes;
src/HOL/Tools/try0.ML src/Pure/Isar/method.ML

2014-08-19 wenzelm [Tue, 19 Aug 2014 15:10:37 +0200] rev 58004
tuned;
src/Pure/Isar/method.ML src/Pure/Isar/proof.ML

2014-08-19 wenzelm [Tue, 19 Aug 2014 14:51:25 +0200] rev 58003
clarifed Method.evaluate: turn text into semantic method (like Basic);
src/Pure/Isar/method.ML src/Pure/Isar/proof.ML

2014-08-19 wenzelm [Tue, 19 Aug 2014 12:05:11 +0200] rev 58002
simplified type Proof.method;
src/HOL/Fun_Def.thy src/HOL/Nominal/nominal_induct.ML src/HOL/Nominal/nominal_primrec.ML src/HOL/Tools/coinduction.ML src/Pure/Isar/element.ML src/Pure/Isar/method.ML src/Pure/Isar/proof.ML src/Tools/induct.ML

2014-08-18 wenzelm [Mon, 18 Aug 2014 15:46:27 +0200] rev 58001
more general dummy: may contain "parked arguments", for example;
src/Pure/more_thm.ML

2014-08-19 desharna [Tue, 19 Aug 2014 16:46:33 +0200] rev 58000
document 'ctr_transfer'
src/Doc/Datatypes/Datatypes.thy

2014-08-19 desharna [Tue, 19 Aug 2014 16:46:31 +0200] rev 57999
generate 'ctr_transfer' for (co)datatypes
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML