--- /dev/null
+<?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>
+
projects / helm.git / blobdiff