[df]rule methods;
authorwenzelm
Wed Feb 09 12:30:25 2000 +0100 (2000-02-09)
changeset 8220e04928747b18
parent 8219 504689622489
child 8221 6be623684675
[df]rule methods;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Wed Feb 09 12:30:04 2000 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Feb 09 12:30:25 2000 +0100
     1.3 @@ -38,9 +38,10 @@
     1.4    val multi_resolve: thm list -> thm -> thm Seq.seq
     1.5    val multi_resolves: thm list -> thm list -> thm 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 +  val frule: thm list -> Proof.method
    1.12    val this: Proof.method
    1.13    val assumption: Proof.context -> Proof.method
    1.14    exception METHOD_FAIL of (string * Position.T) * exn
    1.15 @@ -269,15 +270,16 @@
    1.16      else op @ (LocalRules.get ctxt);
    1.17    in FINDGOAL (tac rules facts) end);
    1.18  
    1.19 +fun setup raw_tac =
    1.20 +  let val tac = gen_rule_tac raw_tac
    1.21 +  in (tac, gen_rule tac, gen_rule' tac) end;
    1.22 +
    1.23  in
    1.24  
    1.25 -val rule_tac = gen_rule_tac Tactic.resolve_tac;
    1.26 -val rule = gen_rule rule_tac;
    1.27 -val some_rule = gen_rule' rule_tac;
    1.28 -
    1.29 -val erule_tac = gen_rule_tac Tactic.eresolve_tac;
    1.30 -val erule = gen_rule erule_tac;
    1.31 -val some_erule = gen_rule' erule_tac;
    1.32 +val (rule_tac, rule, some_rule) = setup Tactic.resolve_tac;
    1.33 +val (erule_tac, erule, some_erule) = setup Tactic.eresolve_tac;
    1.34 +val (drule_tac, drule, some_drule) = setup Tactic.dresolve_tac;
    1.35 +val (frule_tac, frule, some_frule) = setup Tactic.forward_tac;
    1.36  
    1.37  end;
    1.38  
    1.39 @@ -519,7 +521,9 @@
    1.40    ("fold", thms_args fold, "fold definitions"),
    1.41    ("default", thms_ctxt_args some_rule, "apply some rule"),
    1.42    ("rule", thms_ctxt_args some_rule, "apply some rule"),
    1.43 -  ("erule", thms_ctxt_args some_erule, "apply some erule (improper!)"),
    1.44 +  ("erule", thms_ctxt_args some_erule, "apply some rule in elimination manner (improper!)"),
    1.45 +  ("drule", thms_ctxt_args some_drule, "apply some rule in destruct manner (improper!)"),
    1.46 +  ("frule", thms_ctxt_args some_frule, "apply some rule in forward manner (improper!)"),
    1.47    ("this", no_args this, "apply current facts as rules"),
    1.48    ("assumption", ctxt_args assumption, "proof by assumption, preferring facts")];
    1.49