src/HOL/Extraction/Pigeonhole.thy
 changeset 21127 c8e862897d13 parent 21062 876dd2695423 child 21404 eb85850d3eb7
```--- a/src/HOL/Extraction/Pigeonhole.thy	Tue Oct 31 14:58:14 2006 +0100
+++ b/src/HOL/Extraction/Pigeonhole.thy	Tue Oct 31 14:58:16 2006 +0100
@@ -16,8 +16,8 @@
We need decidability of equality on natural numbers:
*}

-lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
-  apply (induct m)
+lemma nat_eq_dec: "(m\<Colon>nat) = n \<or> m \<noteq> n"
+  apply (induct m arbitrary: n)
apply (case_tac n)
apply (case_tac [3] n)
apply (simp only: nat.simps, iprover?)+
@@ -307,9 +307,6 @@
arbitrary_nat_subst :: "nat \<times> nat"
"arbitrary_nat_subst = (0, 0)"

-lemma [code func]:
-  "arbitrary_nat = arbitrary_nat" ..
-
code_axioms
arbitrary_nat \<equiv> arbitrary_nat_subst

@@ -317,7 +314,7 @@
"test n = pigeonhole n (\<lambda>m. m - 1)"
"test' n = pigeonhole_slow n (\<lambda>m. m - 1)"

-code_gen test test' "op !" (SML -)
+code_gen test test' "op !" (SML *)

ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"```