| changeset 35275 | 3745987488b2 |
| parent 35230 | be006fbcfb96 |
| parent 35267 | 8dfd816713c6 |
| child 44654 | d80fe56788a5 |
--- a/src/HOL/ex/Arith_Examples.thy Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/ex/Arith_Examples.thy Mon Feb 22 09:17:49 2010 +0100 @@ -33,7 +33,7 @@ *) subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs}, - @{term Algebras.minus}, @{term nat}, @{term Divides.mod}, + @{term minus}, @{term nat}, @{term Divides.mod}, @{term Divides.div} *} lemma "(i::nat) <= max i j"