src/Doc/IsarRef/Spec.thy

   declarations from all dependencies are collected and are presented
   as a local theory.  In this process, which is called \emph{roundup},
   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}.
 *}
 
 
 subsection {* Locale expressions \label{sec:locale-expr} *}