equal
deleted
inserted
replaced
68 (*Print and return a sequence of theorems, separated by blank lines. *) |
68 (*Print and return a sequence of theorems, separated by blank lines. *) |
69 fun prthq thseq = |
69 fun prthq thseq = |
70 (Sequence.prints (fn _ => print_thm) 100000 thseq; thseq); |
70 (Sequence.prints (fn _ => print_thm) 100000 thseq; thseq); |
71 |
71 |
72 (*Print and return a list of theorems, separated by blank lines. *) |
72 (*Print and return a list of theorems, separated by blank lines. *) |
73 fun prths ths = (print_list_ln print_thm ths; ths); |
73 fun prths ths = (seq (fn th => (print_thm th; writeln "")) ths; ths); |
74 |
74 |
75 |
75 |
76 (* other printing commands *) |
76 (* other printing commands *) |
77 |
77 |
78 fun pretty_ctyp cT = |
78 fun pretty_ctyp cT = |