src/FOL/intprover.ML
changeset 702 98fc1a8e832a
parent 0 a5a9c433f639
child 1005 65188e520024
equal deleted inserted replaced
701:74ee8b9ff9a7 702:98fc1a8e832a
    58 			    bimatch_tac safe0_brls,
    58 			    bimatch_tac safe0_brls,
    59 			    hyp_subst_tac,
    59 			    hyp_subst_tac,
    60 			    bimatch_tac safep_brls] ;
    60 			    bimatch_tac safep_brls] ;
    61 
    61 
    62 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
    62 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
    63 val safe_tac = DETERM (REPEAT_FIRST safe_step_tac);
    63 val safe_tac = REPEAT_DETERM_FIRST safe_step_tac;
    64 
    64 
    65 (*These steps could instantiate variables and are therefore unsafe.*)
    65 (*These steps could instantiate variables and are therefore unsafe.*)
    66 val inst_step_tac =
    66 val inst_step_tac =
    67   assume_tac APPEND' mp_tac APPEND' 
    67   assume_tac APPEND' mp_tac APPEND' 
    68   biresolve_tac (safe0_brls @ safep_brls);
    68   biresolve_tac (safe0_brls @ safep_brls);