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