# HG changeset patch
# User nipkow
# Date 1025538128 -7200
# Node ID 2a6ad4357d72fc7e6a5ee336194ae2d62a36b3af
# Parent  a8b5f0df6602cc0e563d58cf559ba19dd2bdb2cd
modified Larry's changes to make div/mod a numeral work in arith.

diff -r a8b5f0df6602 -r 2a6ad4357d72 src/HOL/Integ/IntDiv.thy
--- 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*}