src/Pure/Isar/proof_display.ML
changeset 22335 6c4204df6863
parent 22095 07875394618e
child 22872 d7189dc8939c
     1.1 --- a/src/Pure/Isar/proof_display.ML	Sat Feb 17 17:18:47 2007 +0100
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Sat Feb 17 17:19:59 2007 +0100
     1.3 @@ -22,6 +22,7 @@
     1.4    val pprint_thm: thm -> pprint_args -> unit
     1.5    val print_theorems_diff: theory -> theory -> unit
     1.6    val print_full_theory: bool -> theory -> unit
     1.7 +  val pretty_full_theory: bool -> theory -> Pretty.T
     1.8    val string_of_rule: Proof.context -> string -> thm -> string
     1.9    val print_results: bool -> Proof.context ->
    1.10      ((string * string) * (string * thm list) list) -> unit
    1.11 @@ -72,6 +73,9 @@
    1.12  
    1.13  val print_theory = print_full_theory false;
    1.14  
    1.15 +fun pretty_full_theory verbose thy =
    1.16 +    Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
    1.17 +
    1.18  
    1.19  (* refinement rule *)
    1.20