# HG changeset patch
# User wenzelm
# Date 1433229005 -7200
# Node ID bc0827281dc1e172979a927b609cd13914795fc3
# Parent  f0b2457bf68e386cfa7950c0f5bc354d4391bc65
tuned proof;

diff -r f0b2457bf68e -r bc0827281dc1 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Mon Jun 01 18:07:36 2015 +0200
+++ b/src/HOL/GCD.thy	Tue Jun 02 09:10:05 2015 +0200
@@ -1355,7 +1355,7 @@
 
 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
-  by (auto intro: dvd_antisym [transferred] lcm_least_int)  (* FIXME slow *)
+  using lcm_least_int zdvd_antisym_nonneg by auto
 
 interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
   + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1