cleaned up
authorhaftmann
Tue Oct 31 14:58:16 2006 +0100 (2006-10-31)
changeset 21127c8e862897d13
parent 21126 4dbc3ccbaab0
child 21128 7b2624686fc3
cleaned up
src/HOL/Extraction/Pigeonhole.thy
src/HOL/Tools/datatype_package.ML
     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  
    2.22  (* add_cases_induct *)