equal
deleted
inserted
replaced
81 fun swapify intrs = intrs RLN (2, [swap]); 
81 fun swapify intrs = intrs RLN (2, [swap]); 
82 
82 
83 (*Uses introduction rules in the normal way, or on negated assumptions, 
83 (*Uses introduction rules in the normal way, or on negated assumptions, 
84 trying rules in order. *) 
84 trying rules in order. *) 
85 fun swap_res_tac rls = 
85 fun swap_res_tac rls = 
86 let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap)) 
86 let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls 
87 in assume_tac ORELSE' contr_tac ORELSE' FIRST' (map tacf rls) 
87 in assume_tac ORELSE' 

88 contr_tac ORELSE' 

89 biresolve_tac (foldr addrl (rls,[])) 
88 end; 
90 end; 
89 
91 
90 (*Given assumption P>Q, reduces subgoal Q to P [deletes the implication!] *) 
92 (*Given assumption P>Q, reduces subgoal Q to P [deletes the implication!] *) 
91 fun chain_tac i = 
93 fun chain_tac i = 
92 eresolve_tac [imp_elim] i THEN 
94 eresolve_tac [imp_elim] i THEN 