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/Primes.thy
changeset 11464 ddea204de5bc
parent 11374 2badb9b2a8ec
child 11701 3d51fbf81c17 
--- a/src/HOL/Library/Primes.thy	Mon Aug 06 13:12:06 2001 +0200
+++ b/src/HOL/Library/Primes.thy	Mon Aug 06 13:43:24 2001 +0200
@@ -54,7 +54,7 @@
 
 declare gcd.simps [simp del]
 
-lemma gcd_1 [simp]: "gcd (m, 1) = 1"
+lemma gcd_1 [simp]: "gcd (m, 1') = 1"
   apply (simp add: gcd_non_0)
   done
 
@@ -140,8 +140,8 @@
   apply (simp add: gcd_commute [of 0])
   done
 
-lemma gcd_1_left [simp]: "gcd (1, m) = 1"
-  apply (simp add: gcd_commute [of 1])
+lemma gcd_1_left [simp]: "gcd (1', m) = 1"
+  apply (simp add: gcd_commute [of "1'"])
   done
isabelle