Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/GCD.thy
changeset 26304 02fbd0e7954a
parent 25671 5e9d6f77d11a
child 27106 ff27dc6e7d05 
--- a/src/HOL/Library/GCD.thy	Mon Mar 17 18:37:04 2008 +0100
+++ b/src/HOL/Library/GCD.thy	Mon Mar 17 18:37:05 2008 +0100
@@ -224,11 +224,11 @@
 definition
   lcm :: "nat \<times> nat \<Rightarrow> nat"
 where
-  "lcm = (\<lambda>(m, n). m * n div gcd (m, n))"
+  lcm_prim_def: "lcm = (\<lambda>(m, n). m * n div gcd (m, n))"
 
 lemma lcm_def:
   "lcm (m, n) = m * n div gcd (m, n)"
-  unfolding lcm_def by simp
+  unfolding lcm_prim_def by simp
 
 lemma prod_gcd_lcm:
   "m * n = gcd (m, n) * lcm (m, n)"
isabelle