# HG changeset patch
# User haftmann
# Date 1185283249 -7200
# Node ID b188cac107ad2520f6426160388311270e4a5b10
# Parent  f54c0e339061c8611357ea2402b0c310a7196795
renamed lcm_lowest to lcm_least

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)
diff -r f54c0e339061 -r b188cac107ad src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Tue Jul 24 15:20:48 2007 +0200
+++ b/src/HOL/ex/LocaleTest2.thy	Tue Jul 24 15:20:49 2007 +0200
@@ -601,7 +601,7 @@
     apply (rule_tac x = "gcd (x, y)" in exI)
     apply auto [1]
     apply (rule_tac x = "lcm (x, y)" in exI)
-    apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_lowest)
+    apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
     done
   then interpret nat_dvd: dlat ["op dvd :: [nat, nat] => bool"] .
   txt {* Interpretation to ease use of definitions, which are
@@ -615,7 +615,7 @@
     apply (unfold nat_dvd.join_def)
     apply (rule the_equality)
     apply (unfold nat_dvd.is_sup_def)
-    by (auto intro: lcm_dvd1 lcm_dvd2 lcm_lowest)
+    by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
 qed
 
 text {* Interpreted theorems from the locales, involving defined terms. *}