# 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. *}