doc-src/IsarImplementation/Thy/document/Isar.tex

   \item \emph{Special method with cases} with named context additions
   associated with the follow-up goal state.
 
   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.
 
   Example: \hyperlink{method.rule}{\mbox{\isa{rule}}}, which captures the key ideas behind