modified Larry's changes to make div/mod a numeral work in arith.
--- a/src/HOL/Integ/IntDiv.thy Mon Jul 01 16:43:50 2002 +0200
+++ b/src/HOL/Integ/IntDiv.thy Mon Jul 01 17:42:08 2002 +0200
@@ -841,8 +841,8 @@
done
(* Enable arith to deal with div 2 and mod 2: *)
-declare split_zdiv [of _ 2, simplified, arith_split]
-declare split_zmod [of _ 2, simplified, arith_split]
+declare split_zdiv [of _ _ "number_of k", simplified, standard, arith_split]
+declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split]
subsection{*Speeding up the division algorithm with shifting*}