# HG changeset patch
# User wenzelm
# Date 1390429180 -3600
# Node ID 2c9d6d305f14ad1529acb61802833b4c7c2adfaf
# Parent  26385678a8f5107fb826cab561e41e7447d2e13c# Parent  68a829b7f1a4eeaf9c884c56ee9c0c6c15432337
merged

diff -r 68a829b7f1a4 -r 2c9d6d305f14 src/Doc/IsarRef/Spec.thy
--- a/src/Doc/IsarRef/Spec.thy	Wed Jan 22 23:19:10 2014 +0100
+++ b/src/Doc/IsarRef/Spec.thy	Wed Jan 22 23:19:40 2014 +0100
@@ -419,7 +419,7 @@
   redundant locale instances are omitted.  A locale instance is
   redundant if it is subsumed by an instance encountered earlier.  A
   more detailed description of this process is available elsewhere
-  \cite{Ballarin2013}.
+  \cite{Ballarin2014}.
 *}
 
 
diff -r 68a829b7f1a4 -r 2c9d6d305f14 src/Doc/manual.bib
--- a/src/Doc/manual.bib	Wed Jan 22 23:19:10 2014 +0100
+++ b/src/Doc/manual.bib	Wed Jan 22 23:19:40 2014 +0100
@@ -161,14 +161,16 @@
   note          = {\url{http://isabelle.in.tum.de/doc/locales.pdf}}
 }
 
-@article{Ballarin2013,
+@article{Ballarin2014,
   author = {Ballarin, Clemens},
   journal = JAR,
-  note = {Online version; to appear in print.},
   publisher = Springer,
   title = {Locales: A Module System for Mathematical Theories},
+  volume = 52,
+  number = 2,
+  pages = {123--153},
   url = {http://dx.doi.org/10.1007/s10817-013-9284-7},
-  year = {2013}}
+  year = {2014}}
 
 @InCollection{Barendregt-Geuvers:2001,
   author = 	 {H. Barendregt and H. Geuvers},