| changeset 30200 | 0db3a35eab01 |
| parent 28952 | 15a4b2cf8c34 |
| child 30224 | 79136ce06bdb |
--- a/doc-src/TutorialI/Types/Numbers.thy Mon Mar 02 16:54:13 2009 +0100 +++ b/doc-src/TutorialI/Types/Numbers.thy Mon Mar 02 17:26:23 2009 +0100 @@ -147,8 +147,8 @@ @{thm[display] zdiv_zadd1_eq[no_vars]} \rulename{zdiv_zadd1_eq} -@{thm[display] zmod_zadd1_eq[no_vars]} -\rulename{zmod_zadd1_eq} +@{thm[display] mod_add1_eq[no_vars]} +\rulename{mod_add1_eq} @{thm[display] zdiv_zmult1_eq[no_vars]} \rulename{zdiv_zmult1_eq}