src/Pure/Isar/method.ML
changeset 9587 1368ce019457
parent 9565 3eb2ea15cc69
child 9631 f4ebf1ec2df6
     1.1 --- a/src/Pure/Isar/method.ML	Mon Aug 14 14:49:49 2000 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Mon Aug 14 14:50:11 2000 +0200
     1.3 @@ -46,6 +46,7 @@
     1.4    val resolveq_cases_tac: bool -> (thm * string list) Seq.seq
     1.5      -> int -> thm -> (thm * (string * RuleCases.T) list) Seq.seq
     1.6    val rule_tac: thm list -> thm list -> int -> tactic
     1.7 +  val erule_tac: thm list -> thm list -> int -> tactic
     1.8    val rule: thm list -> Proof.method
     1.9    val erule: thm list -> Proof.method
    1.10    val drule: thm list -> Proof.method
    1.11 @@ -621,7 +622,7 @@
    1.12  val pure_methods =
    1.13   [("fail", no_args fail, "force failure"),
    1.14    ("succeed", no_args succeed, "succeed"),
    1.15 -  ("-", no_args insert_facts, "do nothing, inserting current facts only"),
    1.16 +  ("-", no_args insert_facts, "do nothing (insert current facts only)"),
    1.17    ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
    1.18    ("unfold", thms_args unfold, "unfold definitions"),
    1.19    ("fold", thms_args fold, "fold definitions"),