2011-04-17 wenzelm [Sun, 17 Apr 2011 21:17:45 +0200] rev 42380
markup attributes/methods via name space;
eliminated obsolete markup;
src/Pure/General/markup.ML src/Pure/Isar/attrib.ML src/Pure/Isar/method.ML src/Tools/jEdit/src/jedit/isabelle_markup.scala

2011-04-17 wenzelm [Sun, 17 Apr 2011 21:04:22 +0200] rev 42379
tuned signature;
src/Pure/General/name_space.ML src/Pure/Isar/proof_context.ML src/Pure/Syntax/syntax_phases.ML src/Pure/global_theory.ML

2011-04-17 wenzelm [Sun, 17 Apr 2011 20:58:43 +0200] rev 42378
markup facts via name space;
eliminated obsolete markup;
src/Pure/General/markup.ML src/Pure/General/markup.scala src/Pure/Isar/proof_context.ML src/Pure/global_theory.ML src/Tools/jEdit/src/jedit/isabelle_markup.scala

2011-04-17 wenzelm [Sun, 17 Apr 2011 20:25:10 +0200] rev 42377
tuned -- order in memory according to variance;
src/Pure/General/markup.ML

2011-04-17 wenzelm [Sun, 17 Apr 2011 20:15:46 +0200] rev 42376
eliminated obsolete markup -- superseded by generic "entity" markup;
src/Pure/General/markup.ML src/Pure/General/markup.scala src/Pure/Isar/proof_context.ML src/Pure/global_theory.ML src/Pure/sign.ML src/Tools/jEdit/src/jedit/isabelle_markup.scala

2011-04-17 wenzelm [Sun, 17 Apr 2011 19:54:04 +0200] rev 42375
report Name_Space.declare/define, relatively to context;
added "global" variants of context-dependent declarations;
src/HOL/Boogie/Tools/boogie_loader.ML src/HOL/HOLCF/Tools/Domain/domain.ML src/HOL/HOLCF/Tools/Domain/domain_axioms.ML src/HOL/HOLCF/Tools/Domain/domain_induction.ML src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Datatype/datatype_abs_proofs.ML src/HOL/Tools/Nitpick/nitpick_model.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/record.ML src/HOL/Tools/typedef.ML src/Pure/General/name_space.ML src/Pure/Isar/attrib.ML src/Pure/Isar/class.ML src/Pure/Isar/class_declaration.ML src/Pure/Isar/code.ML src/Pure/Isar/expression.ML src/Pure/Isar/generic_target.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/locale.ML src/Pure/Isar/method.ML src/Pure/Isar/object_logic.ML src/Pure/Isar/overloading.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/specification.ML src/Pure/Isar/typedecl.ML src/Pure/Proof/extraction.ML src/Pure/Proof/proof_syntax.ML src/Pure/axclass.ML src/Pure/consts.ML src/Pure/facts.ML src/Pure/global_theory.ML src/Pure/more_thm.ML src/Pure/pure_thy.ML src/Pure/sign.ML src/Pure/simplifier.ML src/Pure/theory.ML src/Pure/thm.ML src/Pure/type.ML

2011-04-17 wenzelm [Sun, 17 Apr 2011 13:47:22 +0200] rev 42374
clarified pretty_parsetree: suppress literal tokens;
src/Pure/Syntax/parser.ML

2011-04-16 wenzelm [Sat, 16 Apr 2011 23:41:58 +0200] rev 42373
PARALLEL_GOALS for simplification within auto_tac;
src/Provers/clasimp.ML

2011-04-16 wenzelm [Sat, 16 Apr 2011 23:41:25 +0200] rev 42372
PARALLEL_GOALS for method "simp_all";
src/Pure/simplifier.ML

2011-04-16 wenzelm [Sat, 16 Apr 2011 23:38:25 +0200] rev 42371
enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);
src/Pure/goal.ML