# 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