modified Larry's changes to make div/mod a numeral work in arith.
authornipkow
Mon, 01 Jul 2002 17:42:08 +0200
changeset 13266 2a6ad4357d72
parent 13265 a8b5f0df6602
child 13267 502f69ea6627
modified Larry's changes to make div/mod a numeral work in arith.
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*}