33 (*Negation is treated as a primitive symbol, with rules notI (introduction), |
33 (*Negation is treated as a primitive symbol, with rules notI (introduction), |
34 not_to_imp (converts the assumption ~P to P-->False), and not_impE |
34 not_to_imp (converts the assumption ~P to P-->False), and not_impE |
35 (handles double negations). Could instead rewrite by not_def as the first |
35 (handles double negations). Could instead rewrite by not_def as the first |
36 step of an intuitionistic proof. |
36 step of an intuitionistic proof. |
37 *) |
37 *) |
38 val safe_brls = sort lessb |
38 val safe_brls = sort (make_ord 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,disjE), |
43 (true,disj_impE), (true,disjE), |