Lines Matching defs:print_string
163 val print_string = TextIO.print;
164 fun print_newline() = print_string "\n";
166 | print_strings (t :: []) = print_string t
167 | print_strings (t :: ts) = (print_string t; print_string ",";
169 fun print_theorem th = (print_string (thm_to_string th); print_newline());
172 | print_terms (t :: ts) = (print_term t; print_string ","; print_terms ts);
175 in (print_string "["; print_terms ant; print_string "] |- ";
179 | print_theorems (t :: ts) = (print_theorem t; print_string "\n";
192 print_string ("Failure in dep_rewrite: "^function^"\n")
266 (print_string "Searching for ";
268 print_string "\n")
282 ( (* if debug_matches then (print_string "SUB_matches: ";
297 (print_string "ONCE_DEPTH_matches: "; print_term tm; print_newline())
323 if gl = [] then print_string "proved\n"
338 (print_string "Trying ";
355 print_string "Found deeper match\n"
362 (print_string "match found:\n";
368 (print_string "Rewriting ";
370 print_string "\n")
379 (print_string "New burden: ";
381 print_string "Revised goal: ";
413 (print_string "DEP_TAC:\nburdens = [";
414 map (fn tm => (print_newline(); print_term tm; print_string ",")) gls;
415 print_string "]\ncurrent goals = [";
416 map (fn g2 => (print_newline(); print_goal g2; print_string ",")) gl2;
417 print_string "]\n")
427 (print_string "Prove: ";
430 print_string "From: ";
443 (print_string "gl1 = \n"; print_goal (hd gl1))