diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Rules/Force.thy
--- a/doc-src/TutorialI/Rules/Force.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Rules/Force.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -1,6 +1,7 @@
 (* ID:         $Id$ *)
-theory Force = Divides: (*Divides rather than Main so that the first proof
-                         isn't done by the nat_divide_cancel_factor simprocs.*)
+theory Force = Main: 
+  (*Use Divides rather than Main to experiment with the first proof.
+    Otherwise, it is done by the nat_divide_cancel_factor simprocs.*)
 
 declare div_mult_self_is_m [simp del];