# HG changeset patch
# User bulwahn
# Date 1504261180 -7200
# Node ID 75c090d0e699003936340ca88adaa8c1d4f38db8
# Parent  acb02fa48ef3f2c1b9652a531207a78b9ae3c70d# Parent  72bb0eefd148470b2f19b6f33721432b4125cef5
merged

diff -r acb02fa48ef3 -r 75c090d0e699 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Sep 01 09:45:56 2017 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Sep 01 12:19:40 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.
 *)