--- a/doc-src/IsarImplementation/Thy/Isar.thy Fri Jan 06 10:19:49 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Isar.thy Fri Jan 06 11:27:49 2012 +0100
@@ -269,8 +269,8 @@
Example: @{method "induct"}, which is also a ``raw'' method since it
operates on the internal representation of simultaneous claims as
- Pure conjunction (\secref{{sec:logic-aux}}), instead of separate
- subgoals (\secref{sec::tactical-goals}).
+ Pure conjunction (\secref{sec:logic-aux}), instead of separate
+ subgoals (\secref{sec:tactical-goals}).
\item \emph{Structured method} with strong emphasis on facts outside
the goal state.
--- a/doc-src/IsarImplementation/Thy/document/Isar.tex Fri Jan 06 10:19:49 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Isar.tex Fri Jan 06 11:27:49 2012 +0100
@@ -379,8 +379,8 @@
Example: \hyperlink{method.induct}{\mbox{\isa{induct}}}, which is also a ``raw'' method since it
operates on the internal representation of simultaneous claims as
- Pure conjunction (\secref{{sec:logic-aux}}), instead of separate
- subgoals (\secref{sec::tactical-goals}).
+ Pure conjunction (\secref{sec:logic-aux}), instead of separate
+ subgoals (\secref{sec:tactical-goals}).
\item \emph{Structured method} with strong emphasis on facts outside
the goal state.