src/HOL/Divides.thy
changeset 33728 cb4235333c30
parent 33364 2bd12592c5e8
child 33730 1755ca4ec022
--- a/src/HOL/Divides.thy	Mon Nov 16 18:33:12 2009 +0000
+++ b/src/HOL/Divides.thy	Tue Nov 17 10:17:53 2009 +0000
@@ -2030,9 +2030,11 @@
                       split_neg_lemma [of concl: "%x y. P y"])
 done
 
-(* Enable arith to deal with div 2 and mod 2: *)
-declare split_zdiv [of _ _ "number_of k", simplified, standard, arith_split]
-declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split]
+(* Enable arith to deal with @{term div} and @{term mod} when
+   these are applied to some constant that is of the form
+   @{term "number_of k"}: *)
+declare split_zdiv [of _ _ "number_of k", standard, arith_split]
+declare split_zmod [of _ _ "number_of k", standard, arith_split]
 
 
 subsubsection{*Speeding up the Division Algorithm with Shifting*}