diff options
| -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 |