diff -r 6061ae1f90f2 -r 9bc16273c2d4 doc-src/TutorialI/Rules/Tacticals.thy
--- a/doc-src/TutorialI/Rules/Tacticals.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Rules/Tacticals.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -1,4 +1,4 @@
-theory Tacticals = Main:
+theory Tacticals imports Main begin
 
 text{*REPEAT*}
 lemma "\<lbrakk>P\<longrightarrow>Q; Q\<longrightarrow>R; R\<longrightarrow>S; P\<rbrakk> \<Longrightarrow> S"