diff -r adaa430fc0f7 -r 0c5cd369a643 src/HOL/GCD.thy --- 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 \ (a::int) dvd d \ b dvd d \ (\e. a dvd e \ b dvd e \ d dvd e) \ 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 \ nat \ nat" + lcm_nat: semilattice_neutr "lcm :: nat \ nat \ nat" 1