renamed with/APP to of/OF;
Thu, 01 Jul 1999 21:19:45 +0200
changeset 6874 747f656e04ec
parent 6873 b123f5522ea1
child 6875 df31250ccb3a
renamed with/APP to of/OF;
--- a/src/Pure/Isar/attrib.ML	Thu Jul 01 17:42:27 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Jul 01 21:19:45 1999 +0200
@@ -262,9 +262,9 @@
   ("untag", (gen_untag, gen_untag), "untag theorem"),
   ("COMP", (global_COMP, local_COMP), "compose rules (no lifting)"),
   ("RS", (global_RS, local_RS), "resolve with rule"),
-  ("APP", (global_APP, local_APP), "resolve rule with"),
+  ("OF", (global_APP, local_APP), "resolve with rule -- apply rule to rules"),
   ("where", (global_where, local_where), "named instantiation of theorem"),
-  ("with", (global_with, local_with), "positional instantiation of theorem"),
+  ("of", (global_with, local_with), "positional instantiation of theorem -- apply rule to terms"),
   ("standard", (standard, standard), "put theorem into standard form"),
   ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"),
   ("transfer", (global_transfer, local_transfer), "transfer theorem to this theory")];