<?xml version="1.0"?>
-<html xmlns="http://www.w3.org/1999/xhtml" xmlns:ht="http://www.cs.unibo.it/helm/namespaces/helm-theory" xmlns:helm="http://www.cs.unibo.it/helm" xml:lang="en" lang="en">
-<head>
-<title>Moogle_help</title>
-</head>
-<body bgcolor="#ffffff">
-<helm:uwobo_form>
- <helm:hidden_params />
- <input type="hidden" name="advanced" value="@ADVANCED@"/>
- <input type="hidden" name="keys" value="S,T1,T2,L,RT,E"/>
- <table cellspacing="0" cellpadding="0">
- <tr valign="middle">
- <td><img src="@SEARCH_ENGINE_URL@/getpage?url=moogle_small.png" alt="moogle" /></td>
- <td>  </td>
- <td align="center">
- <input maxLength="256" size="55" name="param.expression" value="@EXPRESSION@" />
- </td>
- <td>
- <input type="submit" value="locate" name="param.action" />
- <input type="submit" value=" hint " name="param.action" />
- <input type="submit" value="match" name="param.action" />
- <input type="submit" value=" elim " name="param.action" />
- </td>
- <td>   </td>
- <td>
- <font size="-2">
- <a href="@SEARCH_ENGINE_URL@/getpage?url=help.html">Help</a><br />
- <a href="@SEARCH_ENGINE_URL@/getpage?url=syntax.html">Input Syntax</a>
- </font>
- </td>
- </tr>
- <tr>
- </tr>
- <tr>
- <td> </td>
- <td> </td>
- <td align="center">
- <font size="-1">
- <input id="all" type="radio" name="param.advanced" value="no" checked="true" />
- <label for="all">Simple search</label>
- <input id="standard" type="radio" name="param.advanced" value="yes" />
- <label for="standard">Advanced search</label>
- </font>
- </td>
- <td> </td>
- <td> </td>
- </tr>
- </table>
-</helm:uwobo_form>
-<hr />
-
-<ul>
- <input type="submit" value="hint" onclick="location:#hint"/>
- <li><a href ="#lhint">hint</a>
- <li><a href ="#"></a>
- <li><a href ="#"></a>
- <li><a href ="#"></a>
-
-<p>ccccccccccccc</p>
-</ul>
-
-<p>
- <a name = "locate"><input type="submit" value="locate"</a>
- Locate and display an object by its short name. <br/>
- 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.
-</p>
-
-<p>
- <a name = "hint"><input type="submit" value="hint"</a>
- Given a closed statement G of the form
- <center>
- \forall x<sub>1</sub>:T<sub>1</sub>...x<sub>n</sub>:T<sub>n</sub>.body
- </center>
- 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).
-</p>
-
-</body>
+<html>
+ <body>
+ <table align="center">
+ <tr>
+ <td>
+ <img align="center" src="http://helm.cs.unibo.it/whelp.png" alt="whelp"/>
+ </td>
+ </tr>
+ <tr>
+ <td> </td>
+ </tr>
+ <tr>
+ <td align="center">
+ <h2>Coming soon!</h2>
+ </td>
+ </tr>
+ </table>
+ <br />
+ <br />
+ In the meantime have a look at the
+ <a href="http://mowgli.mowgli.cs.unibo.it:58085/getpage?url=moogle_syntax.html">Input Syntax page</a>
+ for syntax and examples.
+ </body>
</html>
-
projects / helm.git / blobdiff