Lines Matching defs:print_string
161 val print_string = TextIO.print;
162 fun print_newline() = print_string "\n";
164 | print_strings (t :: []) = print_string t
165 | print_strings (t :: ts) = (print_string t; print_string ",";
167 fun print_theorem th = (print_string (thm_to_string th); print_newline());
170 | print_terms (t :: ts) = (print_term t; print_string ","; print_terms ts);
173 in (print_string "["; print_terms ant; print_string "] |- ";
177 | print_theorems (t :: ts) = (print_theorem t; print_string "\n";
190 print_string ("Failure in dep_rewrite: "^function^"\n")
264 (print_string "Searching for ";
266 print_string "\n")
280 ( (* if debug_matches then (print_string "SUB_matches: ";
295 (print_string "ONCE_DEPTH_matches: "; print_term tm; print_newline())
321 if null gl then print_string "proved\n"
336 (print_string "Trying ";
353 print_string "Found deeper match\n"
360 (print_string "match found:\n";
366 (print_string "Rewriting ";
368 print_string "\n")
377 (print_string "New burden: ";
379 print_string "Revised goal: ";
411 (print_string "DEP_TAC:\nburdens = [";
412 map (fn tm => (print_newline(); print_term tm; print_string ",")) gls;
413 print_string "]\ncurrent goals = [";
414 map (fn g2 => (print_newline(); print_goal g2; print_string ",")) gl2;
415 print_string "]\n")
425 (print_string "Prove: ";
428 print_string "From: ";
441 (print_string "gl1 = \n"; print_goal (hd gl1))