diff -r 39bcdf19dd14 -r 608c157d743d src/Doc/Tutorial/Rules/Forward.thy
--- a/src/Doc/Tutorial/Rules/Forward.thy	Mon Jan 27 17:13:33 2014 +0000
+++ b/src/Doc/Tutorial/Rules/Forward.thy	Wed Jan 29 12:51:37 2014 +0000
@@ -1,4 +1,4 @@
-theory Forward imports Primes begin
+theory Forward imports TPrimes begin
 
 text{*\noindent
 Forward proof material: of, OF, THEN, simplify, rule_format.
@@ -166,7 +166,7 @@
 example of "insert"
 *}
 
-lemma relprime_dvd_mult: 
+lemma relprime_dvd_mult:
       "\<lbrakk> gcd k n = 1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m"
 apply (insert gcd_mult_distrib2 [of m k n])
 txt{*@{subgoals[display,indent=0,margin=65]}*}