--- 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
--- 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%
%