doc-src/TutorialI/tutorial.ind

     \subitem type, 5
   \item \isa {vimage_def} (theorem), \bold{111}
 
   \indexspace
 
-  \item Wenzel, Markus, vii
   \item \isa {wf_induct} (theorem), \bold{115}
   \item \isa {wf_inv_image} (theorem), \bold{115}
   \item \isa {wf_less_than} (theorem), \bold{114}
   \item \isa {wf_lex_prod} (theorem), \bold{115}
   \item \isa {wf_measure} (theorem), \bold{115}