src/HOL/Integ/NatBin.thy
changeset 13189 81ed5c6de890
parent 13154 f1097ea60ba4
child 13491 ddf6ae639f21
     1.1 --- a/src/HOL/Integ/NatBin.thy	Thu May 30 10:21:28 2002 +0200
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Fri May 31 07:53:37 2002 +0200
     1.3 @@ -22,9 +22,9 @@
     1.4  use "nat_bin.ML"
     1.5  setup nat_bin_arith_setup
     1.6  
     1.7 -(* Enable arith to deal with div 2 and mod 2: *)
     1.8 -declare split_div[of 2, simplified,arith_split]
     1.9 -declare split_mod[of 2, simplified,arith_split]
    1.10 +(* Enable arith to deal with div/mod k where k is a numeral: *)
    1.11 +declare split_div[of _ _ "number_of k", standard, arith_split]
    1.12 +declare split_mod[of _ _ "number_of k", standard, arith_split]
    1.13  
    1.14  lemma nat_number_of_Pls: "number_of Pls = (0::nat)"
    1.15    by (simp add: number_of_Pls nat_number_of_def)