equal
deleted
inserted
replaced
653 fun idvalue strings = |
653 fun idvalue strings = |
654 issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name, |
654 issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name, |
655 text=[XML.Elem("pgml",[], |
655 text=[XML.Elem("pgml",[], |
656 maps YXML.parse_body strings)] }) |
656 maps YXML.parse_body strings)] }) |
657 |
657 |
658 fun string_of_thm th = Pretty.string_of |
658 fun string_of_thm th = Pretty.string_of (Display.pretty_thm_aux |
659 (Display.pretty_thm_aux |
659 (Syntax.pp_global (Thm.theory_of_thm th)) |
660 (Syntax.pp_global (Thm.theory_of_thm th)) |
660 {quote = false, show_hyps = false, show_status = true} [] th) |
661 false (* quote *) |
|
662 false (* show hyps *) |
|
663 [] (* asms *) |
|
664 th) |
|
665 |
661 |
666 fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name) |
662 fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name) |
667 |
663 |
668 val string_of_thy = Pretty.string_of o ProofDisplay.pretty_full_theory false |
664 val string_of_thy = Pretty.string_of o ProofDisplay.pretty_full_theory false |
669 in |
665 in |