tuned proof;
authorwenzelm
Tue Jun 02 09:10:05 2015 +0200 (2015-06-02)
changeset 60357bc0827281dc1
parent 60336 f0b2457bf68e
child 60358 aebfbcab1eb8
tuned proof;
src/HOL/GCD.thy
     1.1 --- a/src/HOL/GCD.thy	Mon Jun 01 18:07:36 2015 +0200
     1.2 +++ b/src/HOL/GCD.thy	Tue Jun 02 09:10:05 2015 +0200
     1.3 @@ -1355,7 +1355,7 @@
     1.4  
     1.5  lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
     1.6      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
     1.7 -  by (auto intro: dvd_antisym [transferred] lcm_least_int)  (* FIXME slow *)
     1.8 +  using lcm_least_int zdvd_antisym_nonneg by auto
     1.9  
    1.10  interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.11    + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1