diff -r f54c0e339061 -r b188cac107ad src/HOL/Library/GCD.thy --- a/src/HOL/Library/GCD.thy Tue Jul 24 15:20:48 2007 +0200 +++ b/src/HOL/Library/GCD.thy Tue Jul 24 15:20:49 2007 +0200 @@ -252,7 +252,7 @@ shows "m > 0" using assms by (cases m) auto -lemma lcm_lowest: +lemma lcm_least: assumes "m dvd k" and "n dvd k" shows "lcm (m, n) dvd k" proof (cases k)