# HG changeset patch # User huffman # Date 1245338841 25200 # Node ID 78d06ce5d359e81622aa6b93d29cfde80239a00d # Parent 99f08ce977f9f098b18a1913747f48bcac36f8b5 update to use new GCD library diff -r 99f08ce977f9 -r 78d06ce5d359 src/HOL/ex/LocaleTest2.thy --- a/src/HOL/ex/LocaleTest2.thy Thu Jun 18 07:51:15 2009 -0700 +++ b/src/HOL/ex/LocaleTest2.thy Thu Jun 18 08:27:21 2009 -0700 @@ -599,7 +599,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_least) + apply (auto intro: nat_lcm_dvd1 nat_lcm_dvd2 nat_lcm_least) done then interpret nat_dvd: dlat "op dvd :: [nat, nat] => bool" . txt {* Interpretation to ease use of definitions, which are @@ -613,7 +613,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_least) + by (auto intro: nat_lcm_dvd1 nat_lcm_dvd2 nat_lcm_least) qed text {* Interpreted theorems from the locales, involving defined terms. *} @@ -622,7 +622,7 @@ lemma "((x::nat) dvd y & x ~= y) = (x dvd y & x ~= y)" apply (rule nat_dvd.less_def) done thm nat_dvd.meet_left text {* from dlat *} -lemma "gcd x y dvd x" +lemma "gcd x y dvd (x::nat)" apply (rule nat_dvd.meet_left) done