]> matita.cs.unibo.it Git - helm.git/blob - weblib/test.ma
A compiling version (not complete).
[helm.git] / 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  * 
30  * \ 5img class="topimg intext" src="icons/advance.png"\ 6 Advance - executes the next step of the script
31  * \ 5img class="topimg intext" src="icons/retract.png"\ 6 Retract - undoes the execution of the last step of the script
32  * \ 5img class="topimg intext" src="icons/top.png"\ 6 Top - undoes the whole script, returning to the start
33  * \ 5img class="topimg intext" src="icons/position.png"\ 6 Play - executes the script until the current position of the cursor
34  * \ 5img class="topimg intext" src="icons/bottom.png"\ 6 Bottom - executes the whole script, until the end (or an error) is reached
35  * 
36  * \ 5img class="toolbarimg intext" src="icons/add.png"\ 6 New script - creates a new empty script, opening a window to specify where
37  * the script should be placed in the library
38  * \ 5img class="toolbarimg intext" src="icons/folder.png"\ 6 Open script - opens an existing script in the library
39  * \ 5img class="toolbarimg intext" src="icons/save.png"\ 6 Save script - saves the current script
40  * \ 5img class="toolbarimg intext" src="icons/saveas.png"\ 6 Save script as - saves the current script with a new name
41  * \ 5img class="toolbarimg intext" src="icons/upload.png"\ 6 Import local script - allows the user to import a script from the local 
42  * machine into the web interface buffer
43  * \ 5img class="toolbarimg intext" src="icons/check.png"\ 6 Commit - commits user changes to the shared library
44  * \ 5img class="toolbarimg intext" src="icons/refresh.png"\ 6 Update - synchronizes the user working copy by updating it with the 
45  * changes in the shared library
46  * \ 5img class="toolbarimg intext" src="icons/questionmark.png"\ 6 Show log - shows the last warnings/error messages (for debugging purposes)
47  * \ 5img class="toolbarimg intext" src="icons/delete.png"\ 6 Delete hyperlinks - removes all hyperlinks from the script
48  * 
49  * If you are new to Matita and/or interactive theorem proving, we have a 
50  * tutorial in 10 parts for you. To load it:
51  * 1) click on the "Open script" button in the toolbar (the second circular
52  *    button, whose icon shows a folder)
53  * 2) in the dialog box, select the "tutorial/chapter1.ma" script, then 
54  *    press OK (scripts chapter2.ma ... chapter10.ma contain more advanced
55  *    examples that the user is encouraged to try after chapter1.ma)
56  * 3) follow the instructions in the script.
57  *
58  *)