From da36b8c432608290b5df02134d3fbfccfe097e7d Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 4 Sep 2009 15:27:13 +0000
Subject: Add timing messages

---
 etc/isar/AThousandTheorems.thy | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3