Set up arith to deal with div 2 and mod 2.
authornipkow
Wed, 15 May 2002 13:50:38 +0200
changeset 13154 f1097ea60ba4
parent 13153 4b052946b41c
child 13155 dcbf6cb95534
Set up arith to deal with div 2 and mod 2.
src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Wed May 15 13:50:16 2002 +0200
+++ b/src/HOL/Integ/NatBin.thy	Wed May 15 13:50:38 2002 +0200
@@ -22,6 +22,10 @@
 use "nat_bin.ML"
 setup nat_bin_arith_setup
 
+(* Enable arith to deal with div 2 and mod 2: *)
+declare split_div[of 2, simplified,arith_split]
+declare split_mod[of 2, simplified,arith_split]
+
 lemma nat_number_of_Pls: "number_of Pls = (0::nat)"
   by (simp add: number_of_Pls nat_number_of_def)