summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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