equal
deleted
inserted
replaced
87 fun preplay_trace ctxt assmsp concl outcome = |
87 fun preplay_trace ctxt assmsp concl outcome = |
88 let |
88 let |
89 val ctxt = ctxt |> Config.put show_markup true |
89 val ctxt = ctxt |> Config.put show_markup true |
90 val assms = op @ assmsp |
90 val assms = op @ assmsp |
91 val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]") |
91 val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]") |
92 val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms) |
92 val assms = Pretty.enum " and " "using " " shows " (map (Thm.pretty_thm ctxt) assms) |
93 val concl = Syntax.pretty_term ctxt concl |
93 val concl = Syntax.pretty_term ctxt concl |
94 in |
94 in |
95 tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl]))) |
95 tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl]))) |
96 end |
96 end |
97 |
97 |