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)"