--- a/doc-src/IsarImplementation/Thy/document/logic.tex Sat May 10 14:13:03 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Sat May 10 14:13:20 2008 +0200
@@ -438,7 +438,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Primitive connectives and rules \label{sec:prim_rules}%
+\isamarkupsubsection{Primitive connectives and rules \label{sec:prim-rules}%
}
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Sat May 10 14:13:03 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Sat May 10 14:13:20 2008 +0200
@@ -474,7 +474,7 @@
%
\endisadelimmlref
%
-\isamarkupsection{Names%
+\isamarkupsection{Names \label{sec:names}%
}
\isamarkuptrue%
%