diff options
Diffstat (limited to 'etc/isar/AHundredTheorems.thy')
| -rw-r--r-- | etc/isar/AHundredTheorems.thy | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/etc/isar/AHundredTheorems.thy b/etc/isar/AHundredTheorems.thy index b26bf539..ab6ad8fd 100644 --- a/etc/isar/AHundredTheorems.thy +++ b/etc/isar/AHundredTheorems.thy @@ -1,9 +1,10 @@ -theory AHundredTheorems imports Main +theory AHundredTheorems +imports Main begin (* test this *) -ML {* val start = start_timing(); *} +ML {* val start = Timing.start () *} (* ELISP: -- (setq start (current-time)) -- *) lemma foo: "P --> P" by auto @@ -110,10 +111,7 @@ lemma foo100: "P --> P" by auto (* NB: this doesn't work because of comment aggregation *) (* ELISP: -- (message "Time taken: %f seconds" (time-to-seconds (time-since start))) -- *) -ML {* Output.warning (#message (end_timing start)); *} +ML {* warning (Timing.message (Timing.result start)) *} end - - - |