ocaml 3.09 transition

[helm.git] / helm / searchEngine / html / moogle_syntax.html
diff --git a/helm/searchEngine/html/moogle_syntax.html b/helm/searchEngine/html/moogle_syntax.html

index 80e45ca199388b0456054ad03d8b751e1fbf7f5f..7fa0fe380b459b552c393988efbd9325328d4fd5 100644 (file)
--- a/helm/searchEngine/html/moogle_syntax.html
+++ b/helm/searchEngine/html/moogle_syntax.html
@@ -3,18 +3,20 @@
      <style type="text/css">
        ul.spaced li { padding-bottom: 1em; }
        ul.empty li { list-style-type: none; }
+      tt { font-weight: bold; background-color: lightgray; }
+      tt.uri { font-weight: normal; background-color: transparent; }
      </style>
    </head>
    <body>
      <table>
        <tr>
         <td>
-         <img align="center" src="http://helm.cs.unibo.it/moogle.png" alt="moogle" />
+         <img align="center" src="http://helm.cs.unibo.it/whelp.png" alt="whelp" />
         </td>
        </tr>
        <tr>
         <td>
-         <h2>Moogle Input Syntax</h2>
+         <h2>Whelp Input Syntax</h2>
           <ul class="spaced">
             <li>
             <b>locate <em>&lt;pattern&gt;</em></b>
@@ -27,27 +29,66 @@
             <u>Examples:</u>
             <ul class="empty">
               <li> <tt>nat</tt> pattern matches
-             <tt>cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> only
+             <tt class="uri">cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> only
               </li>
               <li> <tt>n?t</tt> pattern matches
-             <tt>cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> and
-             <tt>cic:/Coq/Init/Logic/not.con</tt>
+             <tt class="uri">cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> and
+             <tt class="uri">cic:/Coq/Init/Logic/not.con</tt>
               </li>
               <li> <tt>nat*</tt> pattern matches
-             <tt>cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt>,
-             <tt>cic:/Coq/Init/Peano/nat_case.con</tt> and many more
+             <tt class="uri">cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt>,
+             <tt class="uri">cic:/Coq/Init/Peano/nat_case.con</tt> and many more
               </li>
             </ul>
             </p>
             </li>
             <li>
-           <b>hint</b>
+           <b>match <em>&lt;term&gt;</em></b>
+           <p>
+           <u>Examples:</u>
+           <ul class="empty">
+             <li> <tt>\forall x,y:nat.x+y=y+x</tt>
+             (commutativity of natural plus)
+             </li>
+             <li> <tt>\forall x,y,z:R.x*(y+z)=x*y+x*z</tt>
+             (distributivity of real times over real plus)
+             </li>
+             <li> <tt>nat \to nat \to nat</tt>
+             (all binary functions over naturals)
+             </li>
+           </ul>
+           </p>
             </li>
             <li>
-           <b>match</b>
+           <b>hint <em>&lt;term&gt;</em></b>
+           <p>
+           <u>Examples:</u>
+           <ul class="empty">
+             <li> <tt>\forall n:nat. (fact n) = n * (fact (n - 1))</tt>
+             (how could we prove <em>n! = (n-1)! * n</em> ?)
+             </li>
+             <li> <tt>\forall n:nat.n \lt n+5</tt>
+             (how could we prove <em>n &lt; n + 5</em> ?)
+             </li>
+             <li> <tt>\forall x,y:nat. x*y \lt (S x)*(S y)</tt>
+             (how could we prove <em>x*y &lt; (x+1)*(y+1)</em> ?)
+             </li>
+           </ul>
+           </p>
             </li>
             <li>
-           <b>elim</b>
+           <b>elim <em>&lt;identifier&gt;</em></b>
+           <p>
+           <u>Examples:</u>
+           <ul class="empty">
+             <li> <tt>nat</tt>
+             (induction/elimination principles over natural numbers)
+             </li>
+             <li> <tt>list</tt>
+             (induction/elimination principles over lists)
+             </li>
+           </ul>
+           </p>
             </li>
           </ul>
         </td>