# HG changeset patch
# User wenzelm
# Date 966257411 -7200
# Node ID 1368ce019457b24d63ee58a5925e568976e76cdf
# Parent  f6669dead969a99b10dc9b30d828b834d4eff949
tuned msg;

diff -r f6669dead969 -r 1368ce019457 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Aug 14 14:49:49 2000 +0200
+++ b/src/Pure/Isar/method.ML	Mon Aug 14 14:50:11 2000 +0200
@@ -46,6 +46,7 @@
   val resolveq_cases_tac: bool -> (thm * string list) Seq.seq
     -> int -> thm -> (thm * (string * RuleCases.T) list) Seq.seq
   val rule_tac: thm list -> thm list -> int -> tactic
+  val erule_tac: thm list -> thm list -> int -> tactic
   val rule: thm list -> Proof.method
   val erule: thm list -> Proof.method
   val drule: thm list -> Proof.method
@@ -621,7 +622,7 @@
 val pure_methods =
  [("fail", no_args fail, "force failure"),
   ("succeed", no_args succeed, "succeed"),
-  ("-", no_args insert_facts, "do nothing, inserting current facts only"),
+  ("-", no_args insert_facts, "do nothing (insert current facts only)"),
   ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
   ("unfold", thms_args unfold, "unfold definitions"),
   ("fold", thms_args fold, "fold definitions"),