--- a/doc-src/IsarRef/Thy/Proof.thy Wed May 14 11:17:36 2008 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy Wed May 14 14:43:34 2008 +0200
@@ -607,10 +607,10 @@
\item [@{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"}] performs
positional instantiation of term variables. The terms @{text
"t\<^sub>1, \<dots>, t\<^sub>n"} are substituted for any schematic
- variables occurring in a theorem from left to right; ``@{text
- _}'' (underscore) indicates to skip a position. Arguments following
- a ``@{keyword "concl"}@{text ":"}'' specification refer to positions
- of the conclusion of a rule.
+ variables occurring in a theorem from left to right; ``@{text _}''
+ (underscore) indicates to skip a position. Arguments following a
+ ``@{text "concl:"}'' specification refer to positions of the
+ conclusion of a rule.
\item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots>
x\<^sub>n = t\<^sub>n"}] performs named instantiation of schematic