summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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*}