# HG changeset patch
# User wenzelm
# Date 950095825 -3600
# Node ID e04928747b18a274a04a268b7f7b6154a9c4cf30
# Parent  504689622489040f037fdf6dde24310c2164132c
[df]rule methods;

diff -r 504689622489 -r e04928747b18 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Feb 09 12:30:04 2000 +0100
+++ b/src/Pure/Isar/method.ML	Wed Feb 09 12:30:25 2000 +0100
@@ -38,9 +38,10 @@
   val multi_resolve: thm list -> thm -> thm Seq.seq
   val multi_resolves: thm list -> thm list -> thm 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
+  val frule: thm list -> Proof.method
   val this: Proof.method
   val assumption: Proof.context -> Proof.method
   exception METHOD_FAIL of (string * Position.T) * exn
@@ -269,15 +270,16 @@
     else op @ (LocalRules.get ctxt);
   in FINDGOAL (tac rules facts) end);
 
+fun setup raw_tac =
+  let val tac = gen_rule_tac raw_tac
+  in (tac, gen_rule tac, gen_rule' tac) end;
+
 in
 
-val rule_tac = gen_rule_tac Tactic.resolve_tac;
-val rule = gen_rule rule_tac;
-val some_rule = gen_rule' rule_tac;
-
-val erule_tac = gen_rule_tac Tactic.eresolve_tac;
-val erule = gen_rule erule_tac;
-val some_erule = gen_rule' erule_tac;
+val (rule_tac, rule, some_rule) = setup Tactic.resolve_tac;
+val (erule_tac, erule, some_erule) = setup Tactic.eresolve_tac;
+val (drule_tac, drule, some_drule) = setup Tactic.dresolve_tac;
+val (frule_tac, frule, some_frule) = setup Tactic.forward_tac;
 
 end;
 
@@ -519,7 +521,9 @@
   ("fold", thms_args fold, "fold definitions"),
   ("default", thms_ctxt_args some_rule, "apply some rule"),
   ("rule", thms_ctxt_args some_rule, "apply some rule"),
-  ("erule", thms_ctxt_args some_erule, "apply some erule (improper!)"),
+  ("erule", thms_ctxt_args some_erule, "apply some rule in elimination manner (improper!)"),
+  ("drule", thms_ctxt_args some_drule, "apply some rule in destruct manner (improper!)"),
+  ("frule", thms_ctxt_args some_frule, "apply some rule in forward manner (improper!)"),
   ("this", no_args this, "apply current facts as rules"),
   ("assumption", ctxt_args assumption, "proof by assumption, preferring facts")];