--- a/src/HOL/Import/import_rule.ML Thu Apr 05 08:13:40 2012 +0200
+++ b/src/HOL/Import/import_rule.ML Thu Apr 05 08:43:31 2012 +0200
@@ -339,6 +339,14 @@
snd (Global_Theory.add_thm ((binding, thm'), []) thy)
end
+fun log_timestamp () =
+ let
+ val time = Time.now ()
+ val millis = nth (space_explode "." (Time.fmt 3 time)) 1
+ in
+ Date.fmt "%d.%m.%Y %H:%M:%S." (Date.fromTimeLocal time) ^ millis
+ end
+
fun process_line str tstate =
let
fun process tstate (#"R", [t]) = gettm t tstate |>> refl |-> setth
@@ -416,7 +424,7 @@
gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.lambda t1 t2) |-> settm
| process (thy, state) (#"+", [s]) =
let
- val _ = tracing ("Noting: " ^ s)
+ val _ = tracing ("NOTING " ^ log_timestamp () ^ ": " ^ s)
in
(store_thm (Binding.name (transl_dot s)) (last_thm state) thy, state)
end