--- a/src/Doc/IsarImplementation/Logic.thy Mon Aug 26 11:41:17 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy Mon Aug 26 11:42:35 2013 +0200
@@ -1173,7 +1173,7 @@
This corresponds to the rule attribute @{attribute THEN} in Isar
source language.
- \item @{text "rule\<^sub>1 RS rule\<^sub>2"} abbreviates @{text "rule\<^sub>1 RS (1,
+ \item @{text "rule\<^sub>1 RS rule\<^sub>2"} abbreviates @{text "rule\<^sub>1 RSN (1,
rule\<^sub>2)"}.
\item @{text "rules\<^sub>1 RLN (i, rules\<^sub>2)"} joins lists of rules. For