2009-03-19 wenzelm [Thu, 19 Mar 2009 15:44:14 +0100] rev 30589
Antiquote.Text: keep full position information;
src/Pure/General/antiquote.ML src/Pure/ML/ml_context.ML src/Pure/Thy/latex.ML src/Pure/Thy/thy_output.ML

2009-03-19 wenzelm [Thu, 19 Mar 2009 15:22:53 +0100] rev 30588
OuterLex.read_antiq;
src/Pure/ML/ml_context.ML src/Pure/Thy/thy_output.ML

2009-03-19 wenzelm [Thu, 19 Mar 2009 15:22:53 +0100] rev 30587
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
src/Pure/General/ROOT.ML src/Pure/General/antiquote.ML src/Pure/IsaMakefile src/Pure/Isar/ROOT.ML src/Pure/Isar/antiquote.ML

2009-03-19 wenzelm [Thu, 19 Mar 2009 15:22:53 +0100] rev 30586
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
scan_comment: recovered change_prompt;
moved read_antiq to outer_lex.ML;
src/Pure/General/symbol_pos.ML src/Pure/Isar/outer_lex.ML

2009-03-19 wenzelm [Thu, 19 Mar 2009 13:28:55 +0100] rev 30585
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
src/Pure/Isar/class.ML src/Pure/Isar/constdefs.ML src/Pure/Isar/element.ML src/Pure/Isar/expression.ML src/Pure/Isar/local_defs.ML src/Pure/Isar/locale.ML src/Pure/Isar/obtain.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/specification.ML src/Pure/sign.ML

2009-03-19 wenzelm [Thu, 19 Mar 2009 13:26:19 +0100] rev 30584
Name.of_binding: proper full_name (with checks) before projecting base name;
src/Pure/name.ML

2009-03-19 wenzelm [Thu, 19 Mar 2009 11:51:49 +0100] rev 30583
merged

2009-03-19 huffman [Thu, 19 Mar 2009 01:29:19 -0700] rev 30582
imported patch euclidean
src/HOL/Library/Determinants.thy src/HOL/Library/Euclidean_Space.thy src/HOL/Library/Finite_Cartesian_Product.thy src/HOL/Library/Topology_Euclidean_Space.thy

2009-03-18 ballarin [Wed, 18 Mar 2009 22:17:23 +0100] rev 30581
Merged.

2009-03-18 ballarin [Wed, 18 Mar 2009 22:14:58 +0100] rev 30580
Updated chapters 1-5 to locale reimplementation.
doc-src/Locales/Locales/Examples.thy doc-src/Locales/Locales/Examples1.thy doc-src/Locales/Locales/Examples2.thy doc-src/Locales/Locales/Examples3.thy doc-src/Locales/Locales/document/Examples.tex doc-src/Locales/Locales/document/Examples1.tex doc-src/Locales/Locales/document/Examples2.tex doc-src/Locales/Locales/document/Examples3.tex