# HG changeset patch
# User ballarin
# Date 1390421667 -3600
# Node ID 26385678a8f5107fb826cab561e41e7447d2e13c
# Parent  c0532866188357baffa3731b70a9ba375f268989
Locales paper has appeared in print.

diff -r c05328661883 -r 26385678a8f5 src/Doc/IsarRef/Spec.thy
--- a/src/Doc/IsarRef/Spec.thy	Wed Jan 22 17:22:26 2014 +0100
+++ b/src/Doc/IsarRef/Spec.thy	Wed Jan 22 21:14:27 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 c05328661883 -r 26385678a8f5 src/Doc/manual.bib
--- a/src/Doc/manual.bib	Wed Jan 22 17:22:26 2014 +0100
+++ b/src/Doc/manual.bib	Wed Jan 22 21:14:27 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},