--- a/src/HOL/GCD.thy Fri Feb 06 17:57:03 2015 +0100
+++ b/src/HOL/GCD.thy Tue Feb 10 14:29:36 2015 +0100
@@ -1398,7 +1398,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)
+ by (auto intro: dvd_antisym [transferred] lcm_least_int) (* FIXME slow *)
interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1