equal
deleted
inserted
replaced
141 val message = |
141 val message = |
142 (case mode of |
142 (case mode of |
143 Auto_Try => "Auto Try0 found a proof" |
143 Auto_Try => "Auto Try0 found a proof" |
144 | Try => "Try0 found a proof" |
144 | Try => "Try0 found a proof" |
145 | Normal => "Try this") ^ ": " ^ |
145 | Normal => "Try this") ^ ": " ^ |
146 Active.sendback_markup [Markup.padding_command] |
146 Active.sendback_markup_command |
147 ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by" |
147 ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by" |
148 else "apply") ^ " " ^ command) ^ |
148 else "apply") ^ " " ^ command) ^ |
149 (case xs of |
149 (case xs of |
150 [(_, ms)] => " (" ^ time_string ms ^ ")." |
150 [(_, ms)] => " (" ^ time_string ms ^ ")." |
151 | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").") |
151 | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").") |