--- 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];