--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy Sun Oct 17 20:00:23 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy Sun Oct 17 20:25:36 2010 +0100
@@ -86,13 +86,12 @@
\framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}}
\end{center}
- \noindent When a definitional package is finished, the auxiliary
- context is reset to the target context. The target now holds
- definitions for terms and theorems that stem from the hypothetical
- @{text "\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by
- the particular target policy (see
- \cite[\S4--5]{Haftmann-Wenzel:2009} for details).
-*}
+ When a definitional package is finished, the auxiliary context is
+ reset to the target context. The target now holds definitions for
+ terms and theorems that stem from the hypothetical @{text
+ "\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by the
+ particular target policy (see \cite[\S4--5]{Haftmann-Wenzel:2009}
+ for details). *}
text %mlref {*
\begin{mldecls}