equal
deleted
inserted
replaced
74 Output.output (Pretty.str_of p) ^ |
74 Output.output (Pretty.str_of p) ^ |
75 "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
75 "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
76 #> space_implode "\\par\\smallskip%\n" |
76 #> space_implode "\\par\\smallskip%\n" |
77 #> enclose "\\isa{" "}"); |
77 #> enclose "\\isa{" "}"); |
78 |
78 |
79 fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt; |
79 fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt; |
80 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; |
80 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; |
81 |
81 |
82 in |
82 in |
83 |
83 |
84 val _ = O.add_commands |
84 val _ = O.add_commands |