# HG changeset patch
# User ballarin
# Date 1504258412 -7200
# Node ID 72bb0eefd148470b2f19b6f33721432b4125cef5
# Parent  e5b1d4d55bf623897da7425cb3e9b0625a883c64
Update header of locale.ML

diff -r e5b1d4d55bf6 -r 72bb0eefd148 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 31 21:48:03 2017 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Sep 01 11:33:32 2017 +0200
@@ -5,23 +5,28 @@
 
 Draws basic ideas from Florian Kammueller's original version of
 locales, but uses the richer infrastructure of Isar instead of the raw
-meta-logic.  Furthermore, structured import of contexts (with merge
-and rename operations) are provided, as well as type-inference of the
-signature parts, and predicate definitions of the specification text.
+meta-logic.  Furthermore, structured composition of contexts (with merge
+and instantiation) is provided, as well as type-inference of the
+signature parts and predicate definitions of the specification text.
 
-Interpretation enables the reuse of theorems of locales in other
-contexts, namely those defined by theories, structured proofs and
-locales themselves.
+Interpretation enables the transfer of declarations and theorems to other
+contexts, namely those defined by theories, structured proofs and locales
+themselves.
+
+A comprehensive account of locales is available:
+
+[1] Clemens Ballarin. Locales: a module system for mathematical theories.
+    Journal of Automated Reasoning, 52(2):123–153, 2014.
 
 See also:
 
-[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
+[2] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
     In Stefano Berardi et al., Types for Proofs and Programs: International
     Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
-[2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
+[3] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
     Dependencies between Locales. Technical Report TUM-I0607, Technische
     Universitaet Muenchen, 2006.
-[3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
+[4] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
     Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
     pages 31-43, 2006.
 *)