# HG changeset patch # User wenzelm # Date 1144764008 -7200 # Node ID 8e207f5602409624e019f688f01e5306a6c5788d # Parent 9aef7314316916ddd98fe14b2dbcb0b7703539a0 export pretty_classrel/arity; diff -r 9aef73143169 -r 8e207f560240 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Apr 11 16:00:07 2006 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Apr 11 16:00:08 2006 +0200 @@ -26,6 +26,8 @@ val pretty_term: context -> term -> Pretty.T val pretty_typ: context -> typ -> Pretty.T val pretty_sort: context -> sort -> Pretty.T + val pretty_classrel: context -> class list -> Pretty.T + val pretty_arity: context -> arity -> Pretty.T val pp: context -> Pretty.pp val pretty_thm: context -> thm -> Pretty.T val pretty_thms: context -> thm list -> Pretty.T