# HG changeset patch
# User wenzelm
# Date 1325845669 -3600
# Node ID 4b9d4659228a22068f134b2d9f09595a51463530
# Parent  d9fe85d3d2cd7e494e25017ff353a977d7d7d9f5
proper refs;

diff -r d9fe85d3d2cd -r 4b9d4659228a doc-src/IsarImplementation/Thy/Isar.thy
--- 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.
diff -r d9fe85d3d2cd -r 4b9d4659228a doc-src/IsarImplementation/Thy/document/Isar.tex
--- 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.