]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/topLevel/Readme
some small improvements: command line sintax changed, -MB added
[helm.git] / helm / gTopLevel / topLevel / Readme
index a59bba799bcee0885e69b323b498bef35d03abaf..1607e5d835a87ec8598f27ec1b9570d71d19e63c 100644 (file)
@@ -6,10 +6,12 @@ L'input puo' contenere piu' di un termine CIC (usare ; per separare).
 
 Sintassi: topLevel <opzioni> 
 
-Opzioni : -locate <nome>     : invocazione do Locate
-          -backward <indice> : invocazione di Backward
-          -show              : mostra solo i termini CIC nell'input
-          -test <indice>     : mostra l'attribuzione dei livelli per
-                               la backward, ma non la esegue 
+Opzioni : -display            : mostra solo i termini CIC nell'input
+          -typeof <URI>       : mostra il tipo dell'oggetto indicato
+                               non riconosce tipi induttivi e prove incomplete
+          -levels <indice>    : mostra l'attribuzione dei livelli
+          -locate <nome>      : invocazione di Locate
+          -backward <indice>  : invocazione di Backward
+         -mbackward <indice> : invoca le Backward con indice da <indice> a 0
 
-le opzioni si possono anche scrivere -l -b -s e -t
\ No newline at end of file
+le opzioni si possono anche scrivere -d -t -l -L -B e -MB nell'ordine.