src/FOLP/intprover.ML
changeset 2572 8a47f85e7a03
parent 1463 49ca5e875691
child 2603 4988dda71c0b
equal deleted inserted replaced
2571:b9f641195b48 2572:8a47f85e7a03
    38 val safe_brls = sort lessb 
    38 val safe_brls = sort lessb 
    39     [ (true,FalseE), (false,TrueI), (false,refl),
    39     [ (true,FalseE), (false,TrueI), (false,refl),
    40       (false,impI), (false,notI), (false,allI),
    40       (false,impI), (false,notI), (false,allI),
    41       (true,conjE), (true,exE),
    41       (true,conjE), (true,exE),
    42       (false,conjI), (true,conj_impE),
    42       (false,conjI), (true,conj_impE),
    43       (true,disj_impE), (true,ex_impE),
    43       (true,disj_impE), (true,disjE), 
    44       (true,disjE), (false,iffI), (true,iffE), (true,not_to_imp) ];
    44       (false,iffI), (true,iffE), (true,not_to_imp) ];
    45 
    45 
    46 val haz_brls =
    46 val haz_brls =
    47     [ (false,disjI1), (false,disjI2), (false,exI), 
    47     [ (false,disjI1), (false,disjI2), (false,exI), 
    48       (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE),
    48       (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE),
    49       (true,all_impE), (true,impE) ];
    49       (true,all_impE), (true,ex_impE), (true,impE) ];
    50 
    50 
    51 (*0 subgoals vs 1 or more: the p in safep is for positive*)
    51 (*0 subgoals vs 1 or more: the p in safep is for positive*)
    52 val (safe0_brls, safep_brls) =
    52 val (safe0_brls, safep_brls) =
    53     partition (apl(0,op=) o subgoals_of_brl) safe_brls;
    53     partition (apl(0,op=) o subgoals_of_brl) safe_brls;
    54 
    54