equal
deleted
inserted
replaced
20 val pprint_ctyp: ctyp -> pprint_args -> unit |
20 val pprint_ctyp: ctyp -> pprint_args -> unit |
21 val pprint_cterm: cterm -> pprint_args -> unit |
21 val pprint_cterm: cterm -> pprint_args -> unit |
22 val pprint_thm: thm -> pprint_args -> unit |
22 val pprint_thm: thm -> pprint_args -> unit |
23 val print_theorems_diff: theory -> theory -> unit |
23 val print_theorems_diff: theory -> theory -> unit |
24 val print_full_theory: bool -> theory -> unit |
24 val print_full_theory: bool -> theory -> unit |
|
25 val pretty_full_theory: bool -> theory -> Pretty.T |
25 val string_of_rule: Proof.context -> string -> thm -> string |
26 val string_of_rule: Proof.context -> string -> thm -> string |
26 val print_results: bool -> Proof.context -> |
27 val print_results: bool -> Proof.context -> |
27 ((string * string) * (string * thm list) list) -> unit |
28 ((string * string) * (string * thm list) list) -> unit |
28 val present_results: Proof.context -> |
29 val present_results: Proof.context -> |
29 ((string * string) * (string * thm list) list) -> unit |
30 ((string * string) * (string * thm list) list) -> unit |
69 |
70 |
70 fun print_full_theory verbose thy = |
71 fun print_full_theory verbose thy = |
71 Pretty.writeln (Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy])); |
72 Pretty.writeln (Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy])); |
72 |
73 |
73 val print_theory = print_full_theory false; |
74 val print_theory = print_full_theory false; |
|
75 |
|
76 fun pretty_full_theory verbose thy = |
|
77 Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]); |
74 |
78 |
75 |
79 |
76 (* refinement rule *) |
80 (* refinement rule *) |
77 |
81 |
78 fun pretty_rule ctxt s thm = |
82 fun pretty_rule ctxt s thm = |