Lines Matching defs:simplify
65 fun simplify (Not p) = simplify1 (Not (simplify p))
66 | simplify (And (p, q)) = simplify1 (And (simplify p, simplify q))
67 | simplify (Or (p, q)) = simplify1 (Or (simplify p, simplify q))
68 | simplify (Imp (p, q)) = simplify1 (Imp (simplify p, simplify q))
69 | simplify (Iff (p, q)) = simplify1 (Iff (simplify p, simplify q))
70 | simplify (Forall (x, p)) = simplify1 (Forall (x, simplify p))
71 | simplify (Exists (x, p)) = simplify1 (Exists (x, simplify p))
72 | simplify fm = fm;
140 val pnf = prenex o nnf o simplify;
167 val full_skolemize = specialize o prenex o skolemize o nnf o simplify;
200 skolemize o nnf o simplify;