# HG changeset patch
# User wenzelm
# Date 1377510155 -7200
# Node ID 09e8c42dbb061bc0e80a208299c081cfe230fab9
# Parent  7a9fe70c8b0a28a4e9fc06d6608d50e4a76ffab1
tuned unchecked ML;

diff -r 7a9fe70c8b0a -r 09e8c42dbb06 src/Doc/IsarImplementation/Logic.thy
--- 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