| changeset 11480 | 0fba0357c04c |
| parent 11407 | 138919f1a135 |
| child 11711 | ecdfd237ffee |
--- a/doc-src/TutorialI/Rules/Forward.thy Wed Aug 08 14:33:10 2001 +0200 +++ b/doc-src/TutorialI/Rules/Forward.thy Wed Aug 08 14:50:28 2001 +0200 @@ -21,12 +21,12 @@ apply (simp add: is_gcd) done -lemma gcd_1 [simp]: "gcd(m,1) = 1" +lemma gcd_1 [simp]: "gcd(m,1') = 1'" apply simp 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 text{*\noindent