X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftest.ma;h=922d36cc25cc155218d095eaccb4e511012c8c9c;hb=9aa2722ff4aa7868ffd14e5a820cd6dc79e2c8a6;hp=362fb6d579c872ce9de48e3ce114069851ce5c47;hpb=fd05d5ee6ec6b74a88f1b6f25319760b4c05ba7c;p=helm.git

diff --git a/weblib/test.ma b/weblib/test.ma
index 362fb6d57..922d36cc2 100644
--- a/weblib/test.ma
+++ b/weblib/test.ma
@@ -1,3 +1,58 @@
-(* prova *)
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.               
+    ||I||                                                                
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2            
+     \ /      
+      V_______________________________________________________________ *)
 
-axiom pippo : Prop.
\ No newline at end of file
+(* 
+ * QUICK START GUIDE
+ * =================
+ * MatitaWeb is a web interface for the Matita interactive theorem prover. 
+ * Its user interface is composed of two main panes: 
+ * 
+ * -> the script area, whose content you are currently reading, which is 
+ *    used to input definitions and theorems to be checked by Matita; 
+ * -> a top area with a title bar and a toolbar providing all the 
+ *    interactive operations apart from proof authoring. 
+ * 
+ * The toolbar on the top is divided in two sections:
+ * -> the large blue tiles provide the basic operations concerning the 
+ *    execution and checking of a proof script, including step-by-step 
+ *    execution 
+ * -> the smaller circular buttons on the right provide script management
+ *    operations (create, open, save...)
+ * 
+ * img class="topimg intext" src="icons/advance.png" Advance - executes the next step of the script
+ * img class="topimg intext" src="icons/retract.png" Retract - undoes the execution of the last step of the script
+ * img class="topimg intext" src="icons/top.png" Top - undoes the whole script, returning to the start
+ * img class="topimg intext" src="icons/position.png" Play - executes the script until the current position of the cursor
+ * img class="topimg intext" src="icons/bottom.png" Bottom - executes the whole script, until the end (or an error) is reached
+ * 
+ * img class="toolbarimg intext" src="icons/add.png" New script - creates a new empty script, opening a window to specify where
+ * the script should be placed in the library
+ * img class="toolbarimg intext" src="icons/folder.png" Open script - opens an existing script in the library
+ * img class="toolbarimg intext" src="icons/save.png" Save script - saves the current script
+ * img class="toolbarimg intext" src="icons/saveas.png" Save script as - saves the current script with a new name
+ * img class="toolbarimg intext" src="icons/upload.png" Import local script - allows the user to import a script from the local 
+ * machine into the web interface buffer
+ * img class="toolbarimg intext" src="icons/check.png" Commit - commits user changes to the shared library
+ * img class="toolbarimg intext" src="icons/refresh.png" Update - synchronizes the user working copy by updating it with the 
+ * changes in the shared library
+ * img class="toolbarimg intext" src="icons/questionmark.png" Show log - shows the last warnings/error messages (for debugging purposes)
+ * img class="toolbarimg intext" src="icons/delete.png" Delete hyperlinks - removes all hyperlinks from the script
+ * 
+ * If you are new to Matita and/or interactive theorem proving, we have a 
+ * tutorial in 10 parts for you. To load it:
+ * 1) click on the "Open script" button in the toolbar (the second circular
+ *    button, whose icon shows a folder)
+ * 2) in the dialog box, select the "tutorial/chapter1.ma" script, then 
+ *    press OK (scripts chapter2.ma ... chapter10.ma contain more advanced
+ *    examples that the user is encouraged to try after chapter1.ma)
+ * 3) follow the instructions in the script.
+ *
+ *)
\ No newline at end of file