equal
deleted
inserted
replaced
139 |
139 |
140 |
140 |
141 (* local theorems *) |
141 (* local theorems *) |
142 |
142 |
143 fun strings_of_thms (Context {thms, ...}) = |
143 fun strings_of_thms (Context {thms, ...}) = |
144 strings_of_items Display.pretty_thm "Local theorems:" (Symtab.dest thms); |
144 strings_of_items (setmp Display.show_hyps false Display.pretty_thm) |
|
145 "Local theorems:" (Symtab.dest thms); |
145 |
146 |
146 val print_thms = seq writeln o strings_of_thms; |
147 val print_thms = seq writeln o strings_of_thms; |
147 |
148 |
148 |
149 |
149 (* main context *) |
150 (* main context *) |