manual commit after active hyperlinks

[helm.git] / weblib / test.ma

diff --git a/weblib/test.ma b/weblib/test.ma
index ab54bb5d19f1b27b8b51aee67500c82253fe8d2c..ce8cc2355739a8d06a2f0e895905983f96a29850 100644 (file)
--- a/weblib/test.ma
+++ b/weblib/test.ma
@@ -1,8 +1,42 @@
-inductive nat : Set ≝
-| O : nat
-| S : nat \ 5span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"\ 6\ 5span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"\ 6\ 5span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"\ 6→\ 5/span\ 6\ 5/span\ 6\ 5/span\ 6 nat.
+(*
+    ||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_______________________________________________________________ *)
+
+(* 
+ * 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...)
+ * Hover the mouse pointer over these elements to show tooltips explaining 
+ * their purpose.
+ * 
+ * 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.
+ *
+ *)
 
-let rec plus n m ≝
-match n with
-[O ⇒ m
-|(S p) ⇒ S (plus p m)].
\ No newline at end of file