Lines Matching defs:pr
205 fun term pr =
207 fun tm (Var v) = pr (varify v)
208 | tm (Fn (f, l)) = (pr (funify (length l) f); tms l)
210 | tms (x :: y) = (pr "("; tm x; app (fn z => (pr ","; tm z)) y)
215 fun literal pr (Not (Atom a)) = (pr "--"; term pr a)
216 | literal pr (Atom a) = (pr "++"; term pr a)
219 fun clause pr ty (cl, n) =
221 val () = if n = 0 then () else pr "\n"
222 val () = pr ("input_clause(clause" ^ int_to_string n ^ "," ^ ty ^ ",\n")
223 val () = pr " [";
226 | x :: y => (literal pr x; app (fn z => (pr ",\n ";literal pr z)) y)
227 val () = pr "]).\n"
236 fun pr x = output (h, x)
237 val () = pr separator
238 val () = pr (name n)
239 val () = pr separator
240 val n = foldl (clause pr "hypothesis") 0 (strip_conj a)
241 val n = foldl (clause pr "conjecture") n (strip_conj b)
243 val () = pr separator