author haftmann Tue Oct 31 14:58:16 2006 +0100 (2006-10-31) changeset 21127 c8e862897d13 parent 21126 4dbc3ccbaab0 child 21128 7b2624686fc3
cleaned up
```     1.1 --- a/src/HOL/Extraction/Pigeonhole.thy	Tue Oct 31 14:58:14 2006 +0100
1.2 +++ b/src/HOL/Extraction/Pigeonhole.thy	Tue Oct 31 14:58:16 2006 +0100
1.3 @@ -16,8 +16,8 @@
1.4  We need decidability of equality on natural numbers:
1.5  *}
1.6
1.7 -lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
1.8 -  apply (induct m)
1.9 +lemma nat_eq_dec: "(m\<Colon>nat) = n \<or> m \<noteq> n"
1.10 +  apply (induct m arbitrary: n)
1.11    apply (case_tac n)
1.12    apply (case_tac [3] n)
1.13    apply (simp only: nat.simps, iprover?)+
1.14 @@ -307,9 +307,6 @@
1.15    arbitrary_nat_subst :: "nat \<times> nat"
1.16    "arbitrary_nat_subst = (0, 0)"
1.17
1.18 -lemma [code func]:
1.19 -  "arbitrary_nat = arbitrary_nat" ..
1.20 -
1.21  code_axioms
1.22    arbitrary_nat \<equiv> arbitrary_nat_subst
1.23
1.24 @@ -317,7 +314,7 @@
1.25    "test n = pigeonhole n (\<lambda>m. m - 1)"
1.26    "test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
1.27
1.28 -code_gen test test' "op !" (SML -)
1.29 +code_gen test test' "op !" (SML *)
1.30
1.31  ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
1.32  ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"
```
```     2.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Oct 31 14:58:14 2006 +0100
2.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Oct 31 14:58:16 2006 +0100
2.3 @@ -305,13 +305,14 @@
2.4
2.5  fun add_rules simps case_thms size_thms rec_thms inject distinct
2.6                    weak_case_congs cong_att =
2.7 -  (snd o PureThy.add_thmss [(("simps", simps), []),
2.8 +  PureThy.add_thmss [(("simps", simps), []),
2.9      (("", flat case_thms @ size_thms @
2.10            flat distinct @ rec_thms), [Simplifier.simp_add]),
2.11 -    (("", size_thms @ rec_thms),             [setmp CodegenData.strict_functyp false (RecfunCodegen.add NONE)]),
2.12 -    (("", flat inject),               [iff_add]),
2.13 -    (("", map name_notE (flat distinct)),  [Classical.safe_elim NONE]),
2.14 -    (("", weak_case_congs),                  [cong_att])]);
2.15 +    (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
2.16 +    (("", flat inject), [iff_add]),
2.17 +    (("", map name_notE (flat distinct)), [Classical.safe_elim NONE]),
2.18 +    (("", weak_case_congs), [cong_att])]
2.19 +  #> snd;
2.20
2.21