src/Pure/Isar/method.ML
changeset 22586 d2008c5f8d99
parent 22134 ab01073210e4
child 22846 fb79144af9a3
     1.1 --- a/src/Pure/Isar/method.ML	Wed Apr 04 00:11:17 2007 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Apr 04 00:11:18 2007 +0200
     1.3 @@ -567,7 +567,7 @@
     1.4    ("fact", thms_ctxt_args fact, "composition by facts from context"),
     1.5    ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
     1.6    ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac,
     1.7 -    "rename parameters of goal (dynamic instantiation)"),
     1.8 +    "rename parameters of goal"),
     1.9    ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
    1.10      "rotate assumptions of goal"),
    1.11    ("tactic", simple_args Args.name tactic, "ML tactic as proof method")]);