changeset 41278 | 8e1cde88aae6 |
parent 41052 | 3db267a01c1d |
child 41772 | 27d4c768cf20 |
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Dec 19 00:13:25 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Dec 19 11:48:42 2010 +0100 @@ -246,6 +246,8 @@ "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n else "goal")) [Logic.list_implies (assm_ts, orig_t)])) + val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S" + o Date.fromTimeLocal o Time.now) val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) else orig_t val tfree_table =