# HG changeset patch
# User wenzelm
# Date 966501584 -7200
# Node ID 7a0f4c2aed0df225377538854e7c0b5c5e691f0f
# Parent  50f1c4222aeacb06b84935ae9e82d548aacbd00e
renamed 'RS' to 'THEN';

diff -r 50f1c4222aea -r 7a0f4c2aed0d src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Aug 17 10:39:30 2000 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Aug 17 10:39:44 2000 +0200
@@ -285,7 +285,7 @@
  [("tag", (gen_tag, gen_tag), "tag theorem"),
   ("untag", (gen_untag, gen_untag), "untag theorem"),
   ("COMP", (global_COMP, local_COMP), "compose rules (no lifting)"),
-  ("RS", (global_RS, local_RS), "resolve with rule"),
+  ("THEN", (global_RS, local_RS), "resolve with rule"),
   ("OF", (global_APP, local_APP), "resolve with rule -- apply rule to rules"),
   ("where", (global_where, local_where), "named instantiation of theorem"),
   ("of", (global_with, local_with), "positional instantiation of theorem -- apply rule to terms"),