X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtopLevel%2FReadme;h=9f0feb7696d2220de5d86bd4339e0a03d7fbdd5c;hb=f3cc1fe99d45cf1f473226d91df36118db638db5;hp=1607e5d835a87ec8598f27ec1b9570d71d19e63c;hpb=795c7a7a2f45650204e6d5a5974a0eedec6af7af;p=helm.git diff --git a/helm/gTopLevel/topLevel/Readme b/helm/gTopLevel/topLevel/Readme index 1607e5d83..9f0feb769 100644 --- a/helm/gTopLevel/topLevel/Readme +++ b/helm/gTopLevel/topLevel/Readme @@ -10,8 +10,9 @@ Opzioni : -display : mostra solo i termini CIC nell'input -typeof : mostra il tipo dell'oggetto indicato non riconosce tipi induttivi e prove incomplete -levels : mostra l'attribuzione dei livelli - -locate : invocazione di Locate + -restricted : non usa il db: vanno solo -d -t -l + -locate : invocazione di Locate -backward : invocazione di Backward -mbackward : invoca le Backward con indice da a 0 -le opzioni si possono anche scrivere -d -t -l -L -B e -MB nell'ordine. +le opzioni si possono anche scrivere -d -t -l -r -L -B e -MB nell'ordine.