tuned comment;
authorwenzelm
Wed, 04 Apr 2007 00:11:18 +0200
changeset 22586 d2008c5f8d99
parent 22585 16af5cb012e7
child 22587 5454b06320fb
tuned comment;
src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Apr 04 00:11:17 2007 +0200
+++ b/src/Pure/Isar/method.ML	Wed Apr 04 00:11:18 2007 +0200
@@ -567,7 +567,7 @@
   ("fact", thms_ctxt_args fact, "composition by facts from context"),
   ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
   ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac,
-    "rename parameters of goal (dynamic instantiation)"),
+    "rename parameters of goal"),
   ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
     "rotate assumptions of goal"),
   ("tactic", simple_args Args.name tactic, "ML tactic as proof method")]);