diff options
author | Makarius Wenzel <makarius@sketis.net> | 2011-09-28 09:35:01 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 2011-09-28 09:35:01 +0000 |
commit | 75a9e6fa64913e49e55557a6db1b50e8dbc7d25f (patch) | |
tree | c78cd5b7c16f86e6aa65e4172a88110181bd75c2 /etc/isar/AThousandTheorems.thy | |
parent | be1b30498101ed929f03eb3548359dba1713e8aa (diff) |
updated tests to Isabelle2011-1;
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 - - |