src/Pure/Isar/proof_display.ML
changeset 20621 29d57880ba00
parent 20311 3666316adad6
child 20889 f625a65bfed5
     1.1 --- a/src/Pure/Isar/proof_display.ML	Tue Sep 19 23:15:24 2006 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Sep 19 23:15:26 2006 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    val pprint_cterm: cterm -> pprint_args -> unit
     1.5    val pprint_thm: thm -> pprint_args -> unit
     1.6    val print_theorems_diff: theory -> theory -> unit
     1.7 +  val print_full_theory: bool -> theory -> unit
     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 @@ -65,8 +66,10 @@
    1.12  
    1.13  val print_theorems = Pretty.writeln o pretty_theorems;
    1.14  
    1.15 -fun print_theory thy =
    1.16 -  Pretty.writeln (Pretty.chunks (Display.pretty_full_theory thy @ [pretty_theorems thy]));
    1.17 +fun print_full_theory verbose thy =
    1.18 +  Pretty.writeln (Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]));
    1.19 +
    1.20 +val print_theory = print_full_theory false;
    1.21  
    1.22  
    1.23  (* refinement rule *)