src/HOL/Integ/NatBin.thy
changeset 13154 f1097ea60ba4
parent 13043 ad1828b479b7
child 13189 81ed5c6de890
     1.1 --- a/src/HOL/Integ/NatBin.thy	Wed May 15 13:50:16 2002 +0200
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Wed May 15 13:50:38 2002 +0200
     1.3 @@ -22,6 +22,10 @@
     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 +
    1.11  lemma nat_number_of_Pls: "number_of Pls = (0::nat)"
    1.12    by (simp add: number_of_Pls nat_number_of_def)
    1.13