--- a/src/HOL/Extraction/Pigeonhole.thy Wed Jun 02 11:36:09 2010 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy Wed Jun 02 15:35:13 2010 +0200
@@ -236,10 +236,6 @@
end
-consts_code
- "default :: nat" ("{* 0::nat *}")
- "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
-
definition
"test n u = pigeonhole n (\<lambda>m. m - 1)"
definition
@@ -247,6 +243,19 @@
definition
"test'' u = pigeonhole 8 (op ! [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
+ML "timeit (@{code test} 10)"
+ML "timeit (@{code test'} 10)"
+ML "timeit (@{code test} 20)"
+ML "timeit (@{code test'} 20)"
+ML "timeit (@{code test} 25)"
+ML "timeit (@{code test'} 25)"
+ML "timeit (@{code test} 500)"
+ML "timeit @{code test''}"
+
+consts_code
+ "default :: nat" ("{* 0::nat *}")
+ "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
+
code_module PH
contains
test = test
@@ -254,27 +263,13 @@
test'' = test''
ML "timeit (PH.test 10)"
-ML "timeit (@{code test} 10)"
-
ML "timeit (PH.test' 10)"
-ML "timeit (@{code test'} 10)"
-
ML "timeit (PH.test 20)"
-ML "timeit (@{code test} 20)"
-
ML "timeit (PH.test' 20)"
-ML "timeit (@{code test'} 20)"
-
ML "timeit (PH.test 25)"
-ML "timeit (@{code test} 25)"
-
ML "timeit (PH.test' 25)"
-ML "timeit (@{code test'} 25)"
-
ML "timeit (PH.test 500)"
-ML "timeit (@{code test} 500)"
-
ML "timeit PH.test''"
-ML "timeit @{code test''}"
end
+