equal
deleted
inserted
replaced
412 |
412 |
413 local |
413 local |
414 |
414 |
415 val string_of_thm = |
415 val string_of_thm = |
416 Output.output o Pretty.setmp_margin 80 Pretty.string_of o |
416 Output.output o Pretty.setmp_margin 80 Pretty.string_of o |
417 Display.pretty_thm_no_quote o #1 o Drule.freeze_thaw; |
417 setmp show_question_marks false Display.pretty_thm_no_quote; |
418 |
418 |
419 fun thm th = preform (prefix_lines " " (html_mode string_of_thm th)); |
419 fun thm th = preform (prefix_lines " " (html_mode string_of_thm th)); |
420 |
420 |
421 fun thm_name "" = "" |
421 fun thm_name "" = "" |
422 | thm_name a = " " ^ name (a ^ ":"); |
422 | thm_name a = " " ^ name (a ^ ":"); |