diff options
Diffstat (limited to 'etc/isar/AThousandTheorems.thy')
| -rw-r--r-- | etc/isar/AThousandTheorems.thy | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/etc/isar/AThousandTheorems.thy b/etc/isar/AThousandTheorems.thy index 233dc1ed..6e565f90 100644 --- a/etc/isar/AThousandTheorems.thy +++ b/etc/isar/AThousandTheorems.thy @@ -1,7 +1,7 @@ theory AThousandTheorems imports Main begin -ML {* val start = start_timing(); *} +ML {* val start = Timing.start () *} (* ELISP: -- (setq start (current-time)) -- *) lemma foo: "P --> P" by auto @@ -1006,10 +1006,8 @@ lemma foo998: "P --> P" by auto lemma foo999: "P --> P" by auto lemma foo1000: "P --> P" by auto -ML {* Output.warning (#message (end_timing start)); *} +ML {* warning (Timing.message (Timing.result start)) *} (* ELISP: -- (message "Time taken: %f seconds" (time-to-seconds (time-since start))) -- *) end - - |