src/HOL/ex/Arith_Examples.thy
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"