Page901.mmp

$( <MM> <PROOF_ASST> THEOREM=reiteration  LOC_AFTER=
*                                                          Page901.mmp

* This is the end of the (main) tutorial text. For now... but you already
  know enough to be very dangerous :-)

  Visit mmj2\mmj2.html for more documentation,
  and mmj2\doc\* contains much, much more!!!

  Some items you might especially study are the following:

  - The Step Selector Search feature is very powerful. You will find
    quite a bit of documentation about it at:

      mmj2\doc\StepSelectorSearch.html

  - You may also wish to study the Theorem Loader feature:

      mmj2/doc/TheoremLoaderOverview.html

  The Theorem Loader allows you to store a proof in ".mmt" format and
  dynamically update the mmj2 Logical System so that the theorem can
  be used in another proof without having to restart mmj2.

  Note also: you can have two or more mmj2 sessions running
  simultaneously! That means that you can switch over to session #2 to
  create a lemma theorem using the Proof Assistant Theorem Loader, and
  then switch back to session #1 and use the new lemma!

  Feel free to look at the "bonus" tutorial page PageLocalRef.mmp
  to learn more about local references, if you're interested.

  In any case, thanks for your time, and we wish you
  good luck in developing new proofs.
$)