# HG changeset patch # User wenzelm # Date 930856785 -7200 # Node ID 747f656e04ec0923967d087952258493211e1ae6 # Parent b123f5522ea1d022fd0ffca10a6f5db31da13d92 renamed with/APP to of/OF; diff -r b123f5522ea1 -r 747f656e04ec src/Pure/Isar/attrib.ML --- 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")];