1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 10:20:31 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 10:34:12 2012 +0200
     1.3 @@ -580,13 +580,8 @@
     1.4  lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
     1.5    by (simp add: divmod_nat_unique divmod_nat_rel_def)
     1.6  
     1.7 -lemma divmod_nat_base:
     1.8 -  assumes "m < n"
     1.9 -  shows "divmod_nat m n = (0, m)"
    1.10 -proof (rule divmod_nat_unique)
    1.11 -  show "divmod_nat_rel m n (0, m)"
    1.12 -    unfolding divmod_nat_rel_def using assms by simp
    1.13 -qed
    1.14 +lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
    1.15 +  by (simp add: divmod_nat_unique divmod_nat_rel_def)
    1.16  
    1.17  lemma divmod_nat_step:
    1.18    assumes "0 < n" and "n \<le> m"