src/HOL/Divides.thy
changeset 33730 1755ca4ec022
parent 33728 cb4235333c30
child 33804 39b494e8c055
     1.1 --- a/src/HOL/Divides.thy	Tue Nov 17 10:18:51 2009 +0000
     1.2 +++ b/src/HOL/Divides.thy	Tue Nov 17 11:10:22 2009 +0000
     1.3 @@ -2030,9 +2030,9 @@
     1.4                        split_neg_lemma [of concl: "%x y. P y"])
     1.5  done
     1.6  
     1.7 -(* Enable arith to deal with @{term div} and @{term mod} when
     1.8 -   these are applied to some constant that is of the form
     1.9 -   @{term "number_of k"}: *)
    1.10 +text {* Enable (lin)arith to deal with @{const div} and @{const mod}
    1.11 +  when 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