src/FOL/intprover.ML
changeset 4440 9ed4098074bc
parent 2601 b301958c465d
child 5203 eb5a1511a07d
equal deleted inserted replaced
4439:02730662e446 4440:9ed4098074bc
    35 (*Negation is treated as a primitive symbol, with rules notI (introduction),
    35 (*Negation is treated as a primitive symbol, with rules notI (introduction),
    36   not_to_imp (converts the assumption ~P to P-->False), and not_impE
    36   not_to_imp (converts the assumption ~P to P-->False), and not_impE
    37   (handles double negations).  Could instead rewrite by not_def as the first
    37   (handles double negations).  Could instead rewrite by not_def as the first
    38   step of an intuitionistic proof.
    38   step of an intuitionistic proof.
    39 *)
    39 *)
    40 val safe_brls = sort lessb 
    40 val safe_brls = sort (make_ord lessb)
    41     [ (true,FalseE), (false,TrueI), (false,refl),
    41     [ (true,FalseE), (false,TrueI), (false,refl),
    42       (false,impI), (false,notI), (false,allI),
    42       (false,impI), (false,notI), (false,allI),
    43       (true,conjE), (true,exE),
    43       (true,conjE), (true,exE),
    44       (false,conjI), (true,conj_impE),
    44       (false,conjI), (true,conj_impE),
    45       (true,disj_impE), (true,disjE), 
    45       (true,disj_impE), (true,disjE),