Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
indicate slow proof (approx. 20s);
authorwenzelm
Tue, 10 Feb 2015 14:29:36 +0100
changeset 59497 0c5cd369a643
parent 59487 adaa430fc0f7
child 59498 50b60f501b05
indicate slow proof (approx. 20s);
src/HOL/GCD.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle