Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed 'RS' to 'THEN';
authorwenzelm
Thu, 17 Aug 2000 10:39:44 +0200
changeset 9630 7a0f4c2aed0d
parent 9629 50f1c4222aea
child 9631 f4ebf1ec2df6
renamed 'RS' to 'THEN';
src/Pure/Isar/attrib.ML file | annotate | diff | comparison | revisions 
--- 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"),
isabelle