src/Provers/classical.ML
changeset 54 3dea30013b58
parent 0 a5a9c433f639
child 469 b571d997178d
--- a/src/Provers/classical.ML	Tue Oct 12 13:39:35 1993 +0100
+++ b/src/Provers/classical.ML	Fri Oct 15 10:04:30 1993 +0100
@@ -83,8 +83,10 @@
 (*Uses introduction rules in the normal way, or on negated assumptions,
   trying rules in order. *)
 fun swap_res_tac rls = 
-    let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap))
-    in  assume_tac ORELSE' contr_tac ORELSE' FIRST' (map tacf rls)
+    let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
+    in  assume_tac 	ORELSE' 
+	contr_tac 	ORELSE' 
+        biresolve_tac (foldr addrl (rls,[]))
     end;
 
 (*Given assumption P-->Q, reduces subgoal Q to P [deletes the implication!] *)