added multi_resolveq, resolveq_tac;
authorwenzelm
Fri Mar 03 21:00:58 2000 +0100 (2000-03-03)
changeset 83354c117393e4e6
parent 8334 7896bcbd8641
child 8336 fdf3ac335f77
added multi_resolveq, resolveq_tac;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Fri Mar 03 18:26:19 2000 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Mar 03 21:00:58 2000 +0100
     1.3 @@ -37,6 +37,8 @@
     1.4    val fold: thm list -> Proof.method
     1.5    val multi_resolve: thm list -> thm -> thm Seq.seq
     1.6    val multi_resolves: thm list -> thm list -> thm Seq.seq
     1.7 +  val multi_resolveq: thm list -> thm Seq.seq -> thm Seq.seq
     1.8 +  val resolveq_tac: thm Seq.seq -> int -> tactic
     1.9    val rule_tac: thm list -> thm list -> int -> tactic
    1.10    val rule: thm list -> Proof.method
    1.11    val erule: thm list -> Proof.method
    1.12 @@ -245,21 +247,24 @@
    1.13  in
    1.14  
    1.15  val multi_resolve = multi_res 1;
    1.16 -fun multi_resolves facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules));
    1.17 +fun multi_resolveq facts rules = Seq.flat (Seq.map (multi_resolve facts) rules);
    1.18 +fun multi_resolves facts = multi_resolveq facts o Seq.of_list;
    1.19  
    1.20  end;
    1.21  
    1.22  
    1.23  (* rule *)
    1.24  
    1.25 +fun gen_resolveq_tac tac rules i st =
    1.26 +  Seq.flat (Seq.map (fn rule => tac [rule] i st) rules);
    1.27 +
    1.28 +val resolveq_tac = gen_resolveq_tac Tactic.resolve_tac;
    1.29 +
    1.30 +
    1.31  local
    1.32  
    1.33  fun gen_rule_tac tac rules [] = tac rules
    1.34 -  | gen_rule_tac tac erules facts =
    1.35 -      let
    1.36 -        val rules = multi_resolves facts erules;
    1.37 -        fun tactic i state = Seq.flat (Seq.map (fn rule => tac [rule] i state) rules);
    1.38 -      in tactic end;
    1.39 +  | gen_rule_tac tac erules facts = gen_resolveq_tac tac (multi_resolves facts erules);
    1.40  
    1.41  fun gen_rule tac rules = METHOD (FINDGOAL o tac rules);
    1.42