weblib/test.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 (*
  13  * QUICK START GUIDE
  14  * =================
  15  * MatitaWeb is a web interface for the Matita interactive theorem prover.
  16  * Its user interface is composed of two main panes:
  17  *
  18  * -> the script area, whose content you are currently reading, which is
  19  *    used to input definitions and theorems to be checked by Matita;
  20  * -> a top area with a title bar and a toolbar providing all the
  21  *    interactive operations apart from proof authoring.
  22  *
  23  * The toolbar on the top is divided in two sections:
  24  * -> the large blue tiles provide the basic operations concerning the
  25  *    execution and checking of a proof script, including step-by-step
  26  *    execution
  27  * -> the smaller circular buttons on the right provide script management
  28  *    operations (create, open, save...)
  29  * Hover the mouse pointer over these elements to show tooltips explaining
  30  * their purpose.
  31  *
  32  * If you are new to Matita and/or interactive theorem proving, we have a
  33  * tutorial in 10 parts for you. To load it:
  34  * 1) click on the "Open script" button in the toolbar (the second circular
  35  *    button, whose icon shows a folder)
  36  * 2) in the dialog box, select the "tutorial/chapter1.ma" script, then
  37  *    press OK (scripts chapter2.ma ... chapter10.ma contain more advanced
  38  *    examples that the user is encouraged to try after chapter1.ma)
  39  * 3) follow the instructions in the script.
  40  *
  41  *)
  42