# HG changeset patch
# User nipkow
# Date 1021463438 -7200
# Node ID f1097ea60ba43f1e09f0a929345ab041a379d489
# Parent  4b052946b41c620c043f664c2cbbb86cda9976a1
Set up arith to deal with div 2 and mod 2.

diff -r 4b052946b41c -r f1097ea60ba4 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)