diff -r 697dcaaf478f -r 0fba0357c04c doc-src/TutorialI/Rules/Forward.thy
--- 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