2 <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">
4 <title>Moogle_help</title>
6 <body bgcolor="#ffffff">
9 <input type="hidden" name="advanced" value="@ADVANCED@"/>
10 <input type="hidden" name="keys" value="S,T1,T2,L,RT,E"/>
11 <table cellspacing="0" cellpadding="0">
13 <td><img src="@SEARCH_ENGINE_URL@/getpage?url=moogle_small.png" alt="moogle" /></td>
16 <input maxLength="256" size="55" name="param.expression" value="@EXPRESSION@" />
19 <input type="submit" value="locate" name="param.action" />
20 <input type="submit" value=" hint " name="param.action" />
21 <input type="submit" value="match" name="param.action" />
22 <input type="submit" value=" elim " name="param.action" />
24 <td>   </td>
27 <a href="@SEARCH_ENGINE_URL@/getpage?url=help.html">Help</a><br />
28 <a href="@SEARCH_ENGINE_URL@/getpage?url=syntax.html">Input Syntax</a>
39 <input id="all" type="radio" name="param.advanced" value="no" checked="true" />
40 <label for="all">Simple search</label>
41 <input id="standard" type="radio" name="param.advanced" value="yes" />
42 <label for="standard">Advanced search</label>
53 <input type="submit" value="hint" onclick="location:#hint"/>
54 <li><a href ="#lhint">hint</a>
63 <a name = "locate"><input type="submit" value="locate"</a>
64 Locate and display an object by its short name. <br/>
66 locating the identifier "nat" gives you back the definition of
67 natural numbers, and locating "plus" returns several (axiomatic and
68 concrete) definitions of the sum.
72 <a name = "hint"><input type="submit" value="hint"</a>
73 Given a closed statement G of the form
75 \forall x<sub>1</sub>:T<sub>1</sub>...x<sub>n</sub>:T<sub>n</sub>.body
77 returns all theorems in the library whose conclusion is a generalization
78 of body, that is all theorems which can be used (as a last step) to prove G
79 (for tecnical reasons, the actual result may be a superset of