doc-src/TutorialI/Types/Numbers.thy
changeset 30200 0db3a35eab01
parent 28952 15a4b2cf8c34
child 30224 79136ce06bdb
equal deleted inserted replaced
30199:1b32021f6d9e 30200:0db3a35eab01
   145 \rulename{neg_mod_bound}
   145 \rulename{neg_mod_bound}
   146 
   146 
   147 @{thm[display] zdiv_zadd1_eq[no_vars]}
   147 @{thm[display] zdiv_zadd1_eq[no_vars]}
   148 \rulename{zdiv_zadd1_eq}
   148 \rulename{zdiv_zadd1_eq}
   149 
   149 
   150 @{thm[display] zmod_zadd1_eq[no_vars]}
   150 @{thm[display] mod_add1_eq[no_vars]}
   151 \rulename{zmod_zadd1_eq}
   151 \rulename{mod_add1_eq}
   152 
   152 
   153 @{thm[display] zdiv_zmult1_eq[no_vars]}
   153 @{thm[display] zdiv_zmult1_eq[no_vars]}
   154 \rulename{zdiv_zmult1_eq}
   154 \rulename{zdiv_zmult1_eq}
   155 
   155 
   156 @{thm[display] zmod_zmult1_eq[no_vars]}
   156 @{thm[display] zmod_zmult1_eq[no_vars]}