# HG changeset patch
# User wenzelm
# Date 1327697789 -3600
# Node ID 48cf461535cf2595febe84a4f15e2b5130a43b4f
# Parent  0de85de15e524099b8204f4dc3335d69531a882f
tuned;

diff -r 0de85de15e52 -r 48cf461535cf doc-src/IsarRef/Thy/ML_Tactic.thy
--- a/doc-src/IsarRef/Thy/ML_Tactic.thy	Fri Jan 27 21:48:40 2012 +0100
+++ b/doc-src/IsarRef/Thy/ML_Tactic.thy	Fri Jan 27 21:56:29 2012 +0100
@@ -171,10 +171,10 @@
   this usually has a different operational behavior: subgoals are
   solved in a different order.
 
-  \medskip Iterated resolution, such as @{ML_text "REPEAT (FIRSTGOAL
-  (resolve_tac \<dots>))"}, is usually better expressed using the @{method
-  intro} and @{method elim} methods of Isar (see
-  \secref{sec:classical}).
+  \medskip Iterated resolution, such as
+  @{ML_text "REPEAT (FIRSTGOAL (resolve_tac ...))"}, is usually better
+  expressed using the @{method intro} and @{method elim} methods of
+  Isar (see \secref{sec:classical}).
 *}
 
 end
diff -r 0de85de15e52 -r 48cf461535cf doc-src/IsarRef/Thy/document/ML_Tactic.tex
--- a/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Fri Jan 27 21:48:40 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Fri Jan 27 21:56:29 2012 +0100
@@ -195,9 +195,10 @@
   this usually has a different operational behavior: subgoals are
   solved in a different order.
 
-  \medskip Iterated resolution, such as \verb|REPEAT (FIRSTGOAL|\isasep\isanewline%
-\verb|  (resolve_tac \<dots>))|, is usually better expressed using the \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} methods of Isar (see
-  \secref{sec:classical}).%
+  \medskip Iterated resolution, such as
+  \verb|REPEAT (FIRSTGOAL (resolve_tac ...))|, is usually better
+  expressed using the \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} methods of
+  Isar (see \secref{sec:classical}).%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %