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/ZF/ex/Primes.thy
changeset 59788 6f7b6adac439
parent 58871 c399ae4b836f
child 60770 240563fbf41d 
--- a/src/ZF/ex/Primes.thy	Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/ex/Primes.thy	Mon Mar 23 21:05:17 2015 +0100
@@ -93,7 +93,7 @@
 lemma gcd_non_0_raw: 
     "[| 0<n;  n \<in> nat |] ==> gcd(m,n) = gcd(n, m mod n)"
 apply (simp add: gcd_def)
-apply (rule_tac P = "%z. ?left (z) = ?right" in transrec [THEN ssubst])
+apply (rule_tac P = "%z. left (z) = right" for left right in transrec [THEN ssubst])
 apply (simp add: ltD [THEN mem_imp_not_eq, THEN not_sym] 
                  mod_less_divisor [THEN ltD])
 done
isabelle