2010-09-07 wenzelm [Tue, 07 Sep 2010 15:03:59 +0200] rev 39170
Isar_Document.reported_positions: exclude proof state output;
src/Pure/PIDE/isar_document.scala

2010-09-07 wenzelm [Tue, 07 Sep 2010 14:53:05 +0200] rev 39169
Document_View: less aggressive background coloring, departing from classic PG highlighting;
tuned colors;
src/Tools/jEdit/src/jedit/document_view.scala

2010-09-07 wenzelm [Tue, 07 Sep 2010 14:08:21 +0200] rev 39168
report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
tuned color;
src/Pure/General/markup.ML src/Pure/General/markup.scala src/Pure/Syntax/lexicon.ML src/Pure/Syntax/syntax.ML src/Tools/jEdit/src/jedit/document_view.scala

2010-09-07 wenzelm [Tue, 07 Sep 2010 13:16:45 +0200] rev 39167
slightly more robust Plugin.stop -- components might refer to Isabelle.system even after shutdown;
src/Tools/jEdit/src/jedit/plugin.scala

2010-09-06 wenzelm [Mon, 06 Sep 2010 22:58:06 +0200] rev 39166
turned show_hyps and show_tags into proper configuration option;
src/Pure/Isar/attrib.ML src/Pure/Isar/element.ML src/Pure/display.ML

2010-09-06 wenzelm [Mon, 06 Sep 2010 22:31:54 +0200] rev 39165
discontinued obsolete ProofContext.prems_limit;
simplified command setup for 'pr' etc.;
doc-src/IsarRef/Thy/Inner_Syntax.thy doc-src/IsarRef/Thy/document/Inner_Syntax.tex src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/proof_context.ML src/Pure/ProofGeneral/preferences.ML

2010-09-06 wenzelm [Mon, 06 Sep 2010 22:08:49 +0200] rev 39164
ML_Context.thm and ML_Context.thms no longer pervasive;
NEWS src/Pure/ML/ml_context.ML

2010-09-06 wenzelm [Mon, 06 Sep 2010 21:33:19 +0200] rev 39163
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
src/Pure/Isar/attrib.ML src/Pure/Syntax/printer.ML src/Pure/Syntax/syn_trans.ML src/Pure/Syntax/syntax.ML src/Pure/config.ML src/Pure/goal_display.ML src/Pure/meta_simplifier.ML src/Pure/unify.ML

2010-09-06 wenzelm [Mon, 06 Sep 2010 19:23:54 +0200] rev 39162
merged
src/HOL/Extraction/Euclid.thy src/HOL/Extraction/Greatest_Common_Divisor.thy src/HOL/Extraction/Higman.thy src/HOL/Extraction/Pigeonhole.thy src/HOL/Extraction/QuotRem.thy src/HOL/Extraction/ROOT.ML src/HOL/Extraction/Util.thy src/HOL/Extraction/Warshall.thy src/HOL/Extraction/document/root.bib src/HOL/Extraction/document/root.tex src/HOL/Lambda/Commutation.thy src/HOL/Lambda/Eta.thy src/HOL/Lambda/InductTermi.thy src/HOL/Lambda/Lambda.thy src/HOL/Lambda/ListApplication.thy src/HOL/Lambda/ListBeta.thy src/HOL/Lambda/ListOrder.thy src/HOL/Lambda/NormalForm.thy src/HOL/Lambda/ParRed.thy src/HOL/Lambda/README.html src/HOL/Lambda/ROOT.ML src/HOL/Lambda/Standardization.thy src/HOL/Lambda/StrongNorm.thy src/HOL/Lambda/Type.thy src/HOL/Lambda/WeakNorm.thy src/HOL/Lambda/document/root.bib src/HOL/Lambda/document/root.tex src/HOL/ex/Hilbert_Classical.thy

2010-09-06 hoelzl [Mon, 06 Sep 2010 15:01:37 +0200] rev 39161
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
src/HOL/Library/Float.thy