doc-src/TutorialI/Rules/Force.thy

-(* ID:         $Id$ *)
 theory Force imports Main begin 
   (*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];