helm/searchEngine/html/moogle_help.html

   1 <?xml version="1.0"?>
   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">
   3 <head>
   4 <title>Moogle_help</title>
   5 </head>
   6 <body bgcolor="#ffffff">
   7 <helm:uwobo_form>
   8   <helm:hidden_params />
   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">
  12   <tr valign="middle">
  13   <td><img src="@SEARCH_ENGINE_URL@/getpage?url=moogle_small.png" alt="moogle" /></td>
  14   <td>&#xA0;&#xA0;</td>
  15   <td align="center">
  16   <input maxLength="256" size="55" name="param.expression" value="@EXPRESSION@" />
  17   </td>
  18   <td>
  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" />
  23   </td>
  24   <td>&#xA0;&#xA0;&#xA0;</td>
  25   <td>
  26    <font size="-2">
  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>
  29    </font>
  30   </td>
  31   </tr>
  32   <tr>
  33   </tr>
  34   <tr>
  35    <td> </td>
  36    <td> </td>
  37    <td align="center">
  38     <font size="-1">
  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>
  43     </font>
  44    </td>
  45    <td> </td>
  46    <td> </td>
  47    </tr>
  48   </table>
  49 </helm:uwobo_form>
  50 <hr />
  51
  52 <ul>
  53  <input type="submit" value="hint" onclick="location:#hint"/>
  54  <li><a href ="#lhint">hint</a>
  55  <li><a href ="#"></a>
  56  <li><a href ="#"></a>
  57  <li><a href ="#"></a>
  58
  59 <p>ccccccccccccc</p>
  60 </ul>
  61
  62 <p>
  63  <a name = "locate"><input type="submit" value="locate"</a>
  64  Locate and display an object by its short name. <br/>
  65  For instance
  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.
  69 </p>
  70
  71 <p>
  72  <a name = "hint"><input type="submit" value="hint"</a>
  73  Given a closed statement G of the form
  74  <center>
  75   \forall x<sub>1</sub>:T<sub>1</sub>...x<sub>n</sub>:T<sub>n</sub>.body
  76  </center>
  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
  80   the expected one).
  81 </p>
  82
  83 </body>
  84 </html>
  85