diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-04 15:27:13 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-04 15:27:13 +0000 |
| commit | da36b8c432608290b5df02134d3fbfccfe097e7d (patch) | |
| tree | 8df32f1cc0b3f74c887c8eba6f6412f430b11389 /etc/isar | |
| parent | 90de29be25c823e2f274a0a5bdaa8d2acda8ad99 (diff) | |
Add timing messages
Diffstat (limited to 'etc/isar')
| -rw-r--r-- | etc/isar/AThousandTheorems.thy | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/etc/isar/AThousandTheorems.thy b/etc/isar/AThousandTheorems.thy index 77be15b0..a56a7bf1 100644 --- a/etc/isar/AThousandTheorems.thy +++ b/etc/isar/AThousandTheorems.thy @@ -1,7 +1,8 @@ theory AThousandLines imports Main begin -(* set global_timing *) +ML {* val start = start_timing(); *} + lemma foo: "P --> P" by auto lemma foo2: "P --> P" by auto @@ -103,6 +104,10 @@ lemma foo97: "P --> P" by auto lemma foo98: "P --> P" by auto lemma foo99: "P --> P" by auto lemma foo100: "P --> P" by auto + + +ML {* #message (end_timing start); *} + lemma foo101: "P --> P" by auto lemma foo102: "P --> P" by auto lemma foo103: "P --> P" by auto @@ -1005,4 +1010,5 @@ lemma foo998: "P --> P" by auto lemma foo999: "P --> P" by auto lemma foo1000: "P --> P" by auto + end |