--- a/src/HOL/Integ/NatBin.thy Fri Mar 02 15:43:23 2007 +0100
+++ b/src/HOL/Integ/NatBin.thy Fri Mar 02 15:43:24 2007 +0100
@@ -813,54 +813,8 @@
subsection {* code generator setup *}
-lemma neg_number_of_Pls:
- "\<not> neg ((number_of Numeral.Pls) \<Colon> int)"
- by auto
-
-lemma neg_number_of_Min:
- "neg ((number_of Numeral.Min) \<Colon> int)"
- by auto
-
-lemmas nat_number_expand = nat_number Let_def if_bool_eq_conj if_True if_False
- neg_number_of_Pls neg_number_of_Min neg_number_of_BIT Nat.plus.simps
-
-ML {*
-structure NumeralNat =
-struct
-
-val nat_number_expand = thms "nat_number_expand";
+lemmas [code inline] = nat_number_of_def
-fun elim_number_of_nat thy ts =
- let
- fun bins_of (Const _) =
- I
- | bins_of (Var _) =
- I
- | bins_of (Free _) =
- I
- | bins_of (Bound _) =
- I
- | bins_of (Abs (_, _, t)) =
- bins_of t
- | bins_of (t as _ $ _) =
- case strip_comb t
- of (Const ("Numeral.number_of",
- Type (_, [_, Type ("nat", [])])), _) => cons t
- | (t', ts) => bins_of t' #> fold bins_of ts;
- val simpset =
- HOL_basic_ss addsimps nat_number_expand;
- in
- []
- |> fold (bins_of o Thm.term_of) ts
- |> map (Simplifier.rewrite simpset o Thm.cterm_of thy)
- end;
-
-end;
-*}
-
-setup {*
- CodegenData.add_inline_proc ("elim_number_of_nat", NumeralNat.elim_number_of_nat)
-*}
subsection {* legacy ML bindings *}