X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2Fhtml%2Fmoogle_help.html;h=7b2a8bd05d2f7334339ca5a0be06b6ba9fe1b554;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=e6252cc28a79ae259dba19fa9ed1a56c7d06ce4a;hpb=13d18f963d7342cfeddf17f3ae222ff1b14404a8;p=helm.git diff --git a/helm/searchEngine/html/moogle_help.html b/helm/searchEngine/html/moogle_help.html index e6252cc28..7b2a8bd05 100644 --- a/helm/searchEngine/html/moogle_help.html +++ b/helm/searchEngine/html/moogle_help.html @@ -1,85 +1,25 @@ - - -Moogle_help - - - - - - - - - - - - - - - - - - - - - - - - -
moogle   - - - - - - -     - - Help
- Input Syntax - -
- - - - - - -
- -
- - - -

- - Locate and display an object by its short name.
- For instance - locating the identifier "nat" gives you back the definition of - natural numbers, and locating "plus" returns several (axiomatic and - concrete) definitions of the sum. -

- -

- - Given a closed statement G of the form -

- \forall x1:T1...xn:Tn.body -
- returns all theorems in the library whose conclusion is a generalization - of body, that is all theorems which can be used (as a last step) to prove G - (for tecnical reasons, the actual result may be a superset of - the expected one). -

- - + + + + + + + + + + + + +
+ whelp +
+

Coming soon!

+
+
+
+ In the meantime have a look at the + Input Syntax page + for syntax and examples. + -