equal
deleted
inserted
replaced
540 val term_ref = ref[] : term list ref |
540 val term_ref = ref[] : term list ref |
541 val mss_ref = ref [] : meta_simpset list ref; |
541 val mss_ref = ref [] : meta_simpset list ref; |
542 val thm_ref = ref [] : thm list ref; |
542 val thm_ref = ref [] : thm list ref; |
543 val tracing = ref false; |
543 val tracing = ref false; |
544 |
544 |
545 fun say s = if !tracing then (output(std_out,s); flush_out std_out) else (); |
545 fun say s = if !tracing then prs s else (); |
546 |
546 |
547 fun print_thms s L = |
547 fun print_thms s L = |
548 (say s; |
548 (say s; |
549 map (fn th => say (string_of_thm th ^"\n")) L; |
549 map (fn th => say (string_of_thm th ^"\n")) L; |
550 say"\n"); |
550 say"\n"); |