author | wenzelm |
Sat, 19 Sep 2015 22:32:26 +0200 | |
changeset 61201 | 94efa2688ff6 |
parent 61200 | a5674da43c2b |
child 61202 | 9e37178084c5 |
child 61205 | c0a5ebecc68b |
--- a/src/HOL/Divides.thy Sat Sep 19 22:32:13 2015 +0200 +++ b/src/HOL/Divides.thy Sat Sep 19 22:32:26 2015 +0200 @@ -733,7 +733,7 @@ with False show ?thesis by simp qed -text \<open>The division rewrite proper – first, trivial results involving @{text 1}\<close> +text \<open>The division rewrite proper -- first, trivial results involving @{text 1}\<close> lemma divmod_trivial [simp, code]: "divmod Num.One Num.One = (numeral Num.One, 0)"