src/Provers/classical.ML
changeset 54 3dea30013b58
parent 0 a5a9c433f639
child 469 b571d997178d
equal deleted inserted replaced
53:f8f37a9a31dc 54:3dea30013b58
    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