Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Arith_Examples.thy
changeset 34974 18b41bba42b5
parent 31101 26c7bb764a38
child 35230 be006fbcfb96
child 35267 8dfd816713c6 
--- a/src/HOL/ex/Arith_Examples.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/ex/Arith_Examples.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -33,7 +33,7 @@
 *)
 
 subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
-           @{term HOL.minus}, @{term nat}, @{term Divides.mod},
+           @{term Algebras.minus}, @{term nat}, @{term Divides.mod},
            @{term Divides.div} *}
 
 lemma "(i::nat) <= max i j"
isabelle