equal
deleted
inserted
replaced
63 |
63 |
64 val comp_arith = binarith @ intarith @ intarithrel @ natarith |
64 val comp_arith = binarith @ intarith @ intarithrel @ natarith |
65 @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"]; |
65 @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"]; |
66 |
66 |
67 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = |
67 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = |
68 let val (xn1,p1) = variant_abs (xn,xT,p) |
68 let val (xn1,p1) = Syntax.variant_abs (xn,xT,p) |
69 in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end; |
69 in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end; |
70 |
70 |
71 fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm |
71 fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm |
72 (CooperProof.proof_of_evalc sg); |
72 (CooperProof.proof_of_evalc sg); |
73 |
73 |