equal
deleted
inserted
replaced
19 val pprint_term: theory -> term -> pprint_args -> unit |
19 val pprint_term: theory -> term -> pprint_args -> unit |
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 string_of_rule: Proof.context -> string -> thm -> string |
25 val string_of_rule: Proof.context -> string -> thm -> string |
25 val print_results: bool -> Proof.context -> |
26 val print_results: bool -> Proof.context -> |
26 ((string * string) * (string * thm list) list) -> unit |
27 ((string * string) * (string * thm list) list) -> unit |
27 val present_results: Proof.context -> |
28 val present_results: Proof.context -> |
28 ((string * string) * (string * thm list) list) -> unit |
29 ((string * string) * (string * thm list) list) -> unit |
63 |
64 |
64 fun pretty_theorems thy = pretty_theorems_diff Symtab.empty thy; |
65 fun pretty_theorems thy = pretty_theorems_diff Symtab.empty thy; |
65 |
66 |
66 val print_theorems = Pretty.writeln o pretty_theorems; |
67 val print_theorems = Pretty.writeln o pretty_theorems; |
67 |
68 |
68 fun print_theory thy = |
69 fun print_full_theory verbose thy = |
69 Pretty.writeln (Pretty.chunks (Display.pretty_full_theory thy @ [pretty_theorems thy])); |
70 Pretty.writeln (Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy])); |
|
71 |
|
72 val print_theory = print_full_theory false; |
70 |
73 |
71 |
74 |
72 (* refinement rule *) |
75 (* refinement rule *) |
73 |
76 |
74 fun pretty_rule ctxt s thm = |
77 fun pretty_rule ctxt s thm = |