src/HOL/ex/Arith_Examples.thy
changeset 60429 d3d1e185cd63
parent 58889 5b7a9633cfa8
child 61343 5b5656a63bd6
     1.1 --- a/src/HOL/ex/Arith_Examples.thy	Thu Jun 11 21:41:55 2015 +0100
     1.2 +++ b/src/HOL/ex/Arith_Examples.thy	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
     1.6             @{term minus}, @{term nat}, @{term Divides.mod},
     1.7 -           @{term Divides.div} *}
     1.8 +           @{term divide} *}
     1.9  
    1.10  lemma "(i::nat) <= max i j"
    1.11    by linarith