author | webertj |

Tue Nov 17 11:10:22 2009 +0000 (2009-11-17) | |

changeset 33730 | 1755ca4ec022 |

parent 33729 | 3101453e0b1c |

child 33736 | ac81358132fd |

Fixed splitting of div and mod on integers (split theorem differed from implementation).

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