Lines Matching refs:os
71 fun os oc s = TextIO.output (oc,s)
76 | a :: m => (f oc a; os oc sep; oiter_aux oc sep f m)
81 if is_vartype ty then os oc (tptp_of_vartype ty)
87 os oc tyops;
89 else (os oc "("; oiter oc "," write_type Args; os oc ")")
96 os oc "s("; write_type oc (type_of tm); os oc ",";
97 os oc (tptp_of_constvar (length argl) rator);
99 else (os oc "("; oiter oc "," write_term argl; os oc ")");
100 os oc ")"
108 os oc (tptp_of_constvar (length argl) rator);
110 else (os oc "("; oiter oc "," write_term_unsafe argl; os oc ")");
111 os oc ")"
117 os oc "![";
118 oiter oc ", " (fn x => (fn v => os x (tptp_of_var 0 v))) vl;
119 os oc "]: ";
124 os oc "?[";
125 oiter oc ", " (fn x => (fn v => os x (tptp_of_var 0 v))) vl;
126 os oc "]: ";
131 os oc "(";
132 write_pred oc l; os oc " & "; write_pred oc r;
133 os oc ")"
137 os oc "(";
138 write_pred oc l; os oc " | "; write_pred oc r;
139 os oc ")"
143 os oc "(";
144 write_pred oc l; os oc " => "; write_pred oc r;
145 os oc ")"
148 (os oc "~ ("; write_pred oc (dest_neg tm); os oc ")")
154 (os oc "("; write_pred oc l; os oc " <=> "; write_pred oc r; os oc ")")
156 (write_term oc l; os oc " = "; write_term oc r)
159 (os oc "p("; write_term oc tm; os oc ")");;
167 else (os oc "!["; oiter oc "," write_type tvl; os oc "]: ");
173 if !readable_flag then os oc "% " else ();
174 os oc ("fof(" ^ tptp_of_thm (name,tm) ^ ", axiom, ");
176 os oc ").\n"
181 if !readable_flag then os oc "% " else ();
182 os oc "fof(conjecture, conjecture, ";
184 os oc ").\n"