doc-src/TutorialI/Types/Numbers.thy
changeset 30224 79136ce06bdb
parent 30200 0db3a35eab01
child 30242 aea5d7fa7ef5
     1.1 --- a/doc-src/TutorialI/Types/Numbers.thy	Tue Mar 03 12:14:52 2009 +1100
     1.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Tue Mar 03 17:05:18 2009 +0100
     1.3 @@ -100,8 +100,8 @@
     1.4  @{thm[display] div_mult1_eq[no_vars]}
     1.5  \rulename{div_mult1_eq}
     1.6  
     1.7 -@{thm[display] mod_mult1_eq[no_vars]}
     1.8 -\rulename{mod_mult1_eq}
     1.9 +@{thm[display] mod_mult_right_eq[no_vars]}
    1.10 +\rulename{mod_mult_right_eq}
    1.11  
    1.12  @{thm[display] div_mult2_eq[no_vars]}
    1.13  \rulename{div_mult2_eq}
    1.14 @@ -147,8 +147,8 @@
    1.15  @{thm[display] zdiv_zadd1_eq[no_vars]}
    1.16  \rulename{zdiv_zadd1_eq}
    1.17  
    1.18 -@{thm[display] mod_add1_eq[no_vars]}
    1.19 -\rulename{mod_add1_eq}
    1.20 +@{thm[display] mod_add_eq[no_vars]}
    1.21 +\rulename{mod_add_eq}
    1.22  
    1.23  @{thm[display] zdiv_zmult1_eq[no_vars]}
    1.24  \rulename{zdiv_zmult1_eq}