equal
deleted
inserted
replaced
46 SOME ctxt => ctxt |
46 SOME ctxt => ctxt |
47 | NONE => Syntax.init_pretty_global (mk_thy ())) |
47 | NONE => Syntax.init_pretty_global (mk_thy ())) |
48 | NONE => Syntax.init_pretty_global (mk_thy ())); |
48 | NONE => Syntax.init_pretty_global (mk_thy ())); |
49 |
49 |
50 fun pp_thm mk_thy th = |
50 fun pp_thm mk_thy th = |
51 Display.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th; |
51 Thm.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th; |
52 |
52 |
53 fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T); |
53 fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T); |
54 fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t); |
54 fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t); |
55 |
55 |
56 fun pp_ctyp mk_thy cT = pp_typ mk_thy (Thm.typ_of cT); |
56 fun pp_ctyp mk_thy cT = pp_typ mk_thy (Thm.typ_of cT); |
213 |
213 |
214 (* refinement rule *) |
214 (* refinement rule *) |
215 |
215 |
216 fun pretty_rule ctxt s thm = |
216 fun pretty_rule ctxt s thm = |
217 Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"), |
217 Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"), |
218 Pretty.fbrk, Display.pretty_thm ctxt thm]; |
218 Pretty.fbrk, Thm.pretty_thm ctxt thm]; |
219 |
219 |
220 val string_of_rule = Pretty.string_of ooo pretty_rule; |
220 val string_of_rule = Pretty.string_of ooo pretty_rule; |
221 |
221 |
222 |
222 |
223 (* goals *) |
223 (* goals *) |