--- a/doc-src/IsarImplementation/Thy/Tactic.thy Mon Oct 18 12:33:13 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy Mon Oct 18 15:35:20 2010 +0100
@@ -180,14 +180,14 @@
\begin{description}
- \item @{ML_type tactic} represents tactics. The well-formedness
- conditions described above need to be observed. See also @{"file"
- "~~/src/Pure/General/seq.ML"} for the underlying implementation of
- lazy sequences.
+ \item Type @{ML_type tactic} represents tactics. The
+ well-formedness conditions described above need to be observed. See
+ also @{"file" "~~/src/Pure/General/seq.ML"} for the underlying
+ implementation of lazy sequences.
- \item @{ML_type "int -> tactic"} represents tactics with explicit
- subgoal addressing, with well-formedness conditions as described
- above.
+ \item Type @{ML_type "int -> tactic"} represents tactics with
+ explicit subgoal addressing, with well-formedness conditions as
+ described above.
\item @{ML no_tac} is a tactic that always fails, returning the
empty sequence.