# HG changeset patch
# User paulson
# Date 1091792144 -7200
# Node ID b860e444c1db4cb93052c78a9cce2ef4b842b11f
# Parent  af3bca62444bf747c5a757902d776aec0010b751
RS -> THEN

diff -r af3bca62444b -r b860e444c1db src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Aug 06 13:35:26 2004 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Aug 06 13:35:44 2004 +0200
@@ -177,13 +177,13 @@
 val COMP_local = gen_COMP local_thm;
 
 
-(* RS *)
+(* THEN, which corresponds to RS *)
 
 fun resolve (i, B) (x, A) = (x, A RSN (i, B));
 
-fun gen_RS thm = syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm >> resolve);
-val RS_global = gen_RS global_thm;
-val RS_local = gen_RS local_thm;
+fun gen_THEN thm = syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm >> resolve);
+val THEN_global = gen_THEN global_thm;
+val THEN_local = gen_THEN local_thm;
 
 
 (* OF *)
@@ -382,7 +382,7 @@
  [("tagged", (gen_tagged, gen_tagged), "tagged theorem"),
   ("untagged", (gen_untagged, gen_untagged), "untagged theorem"),
   ("COMP", (COMP_global, COMP_local), "direct composition with rules (no lifting)"),
-  ("THEN", (RS_global, RS_local), "resolution with rule"),
+  ("THEN", (THEN_global, THEN_local), "resolution with rule"),
   ("OF", (OF_global, OF_local), "rule applied to facts"),
   ("where", (where_global, where_local), "named instantiation of theorem"),
   ("of", (of_global, of_local), "rule applied to terms"),