equal
deleted
inserted
replaced
194 Proof_Context.pretty_term_abbrev |
194 Proof_Context.pretty_term_abbrev |
195 (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt) |
195 (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt) |
196 (Proofterm.term_of_proof prf); |
196 (Proofterm.term_of_proof prf); |
197 |
197 |
198 fun pretty_standard_proof_of ctxt full thm = |
198 fun pretty_standard_proof_of ctxt full thm = |
199 pretty_proof ctxt |
199 pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm); |
200 (Thm.standard_proof_of {full = full, expand = [Thm.raw_derivation_name thm]} thm); |
|
201 |
200 |
202 end; |
201 end; |