# HG changeset patch
# User wenzelm
# Date 1132684484 -3600
# Node ID 699aad0746e2968930efb37f868c3dd95f1b6681
# Parent  1b191bb611f4a09606e1cb05efe1fcece065cdb3
export map_tags;
added multi_resolve(s) -- from Isar/method.ML;

diff -r 1b191bb611f4 -r 699aad0746e2 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Nov 22 19:34:43 2005 +0100
+++ b/src/Pure/drule.ML	Tue Nov 22 19:34:44 2005 +0100
@@ -93,6 +93,7 @@
   val plain_prop_of: thm -> term
   val add_used: thm -> string list -> string list
   val rule_attribute: ('a -> thm -> thm) -> 'a attribute
+  val map_tags: (tag list -> tag list) -> thm -> thm
   val tag_rule: tag -> thm -> thm
   val untag_rule: string -> thm -> thm
   val tag: tag -> 'a attribute
@@ -142,6 +143,8 @@
   val unvarify: thm -> thm
   val tvars_intr_list: string list -> thm -> (string * (indexname * sort)) list * thm
   val remdups_rl: thm
+  val multi_resolve: thm list -> thm -> thm Seq.seq
+  val multi_resolves: thm list -> thm list -> thm Seq.seq
   val conj_intr: thm -> thm -> thm
   val conj_intr_list: thm list -> thm
   val conj_elim: thm -> thm * thm
@@ -1116,6 +1119,25 @@
 
 
 
+(** multi_resolve **)
+
+local
+
+fun res th i rule =
+  Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty;
+
+fun multi_res _ [] rule = Seq.single rule
+  | multi_res i (th :: ths) rule = Seq.maps (res th i) (multi_res (i + 1) ths rule);
+
+in
+
+val multi_resolve = multi_res 1;
+fun multi_resolves facts rules = Seq.maps (multi_resolve facts) (Seq.of_list rules);
+
+end;
+
+
+
 (** meta-level conjunction **)
 
 local