Merge branch 'main' of https://github.com/jsiek/deduce

gh-pages/pages/reference.html

@@ -329,10 +329,11 @@ <h2 id="definition-proof">Definition (Proof)</h2>
 <div class="code-wrapper"><code id="reference_definition_example"><!-- Generated by codeUtils.js --></code></div>
 <h2 id="definition-and-rewrite-proof">Definition and Rewrite (Proof)</h2>
 <div class="code-wrapper non-deduce"><code>conclusion&nbsp;::=&nbsp;"definition"&nbsp;"{"&nbsp;identifier_list&nbsp;"}"&nbsp;"and"&nbsp;"rewrite"&nbsp;proof_list</code></div>
-<p>Apply the specified definitions to the current goal (see <a href="#definition-proof" target="_self">Definition (Proof)</a>), 
-then the specified rewrites (see <a href="#rewrite-proof" target="_self">Rewrite (Proof)</a>).
-If this simplifies that formula to <code class="inline">true</code>, then this statement proves
-the goal.  Otherwise, Deduce signals an error.</p>
+<p>Apply the specified definitions to the current goal
+(see <a href="#definition-proof" target="_self">Definition (Proof)</a>), then the specified rewrites
+(see <a href="#rewrite-proof" target="_self">Rewrite (Proof)</a>).  If this simplifies that formula
+to <code class="inline">true</code>, then this statement proves the goal.  Otherwise, Deduce
+signals an error.</p>
 <h2 id="definition-in-proof">Definition-In (Proof)</h2>
 <div class="code-wrapper non-deduce"><code>conclusion&nbsp;::=&nbsp;"definition"&nbsp;identifier&nbsp;"in"&nbsp;proof<br>
 conclusion&nbsp;::=&nbsp;"definition"&nbsp;"{"&nbsp;identifier_list&nbsp;"}"&nbsp;"in"&nbsp;proof</code></div>
@@ -751,20 +752,27 @@ <h2 id="reflexive-proof">Reflexive (Proof)</h2>
 <h2 id="rewrite-proof">Rewrite (Proof)</h2>
 <div class="code-wrapper non-deduce"><code>conclusion&nbsp;::=&nbsp;"rewrite"&nbsp;proof_list</code></div>
 <p>Rewrite the current goal formula according to the equalities proved by
-the specified <a href="#proof-list" target="_self">Proof List</a>. For each equality, any term
-in the goal formula that is equal to its left-hand side is replaced by
-its right-hand side. If all the rewriting simplifies the goal formula
-to <code class="inline">true</code>, then this statement proves the goal.  Otherwise, Deduce
-signals an error.</p>
+the specified <a href="#proof-list" target="_self">Proof List</a>. Each equality may be a
+literal equality (has the form <code class="inline">LHS = RHS</code>) or it can be a generalized
+equality (has the form <code class="inline">all x1:T1,...,xn:Tn. LHS = RHS</code>).</p>
+<p>For each equality going left-to-right in the proof list, any subterm
+in the goal formula that matches the left-hand side of the equality
+(<code class="inline">LHS</code>) is replaced by the right-hand side of the equality
+(<code class="inline">RHS</code>). Once a subterm is rewritten by an equality, the resulting
+subterm is not rewritten further by the same equality. On the other
+hand, rewriting with an equality may apply to multiple disjoint
+locations in a formula.</p>
+<p>If the rewriting done by all of the equalities simplifies the goal
+formula to <code class="inline">true</code>, then this statement proves the goal.  Otherwise,
+Deduce signals an error.</p>
 <div class="code-wrapper"><code id="reference_rewrite_example"><!-- Generated by codeUtils.js --></code></div>
 <h2 id="rewrite-in-proof">Rewrite-In (Proof)</h2>
 <div class="code-wrapper non-deduce"><code>conclusion&nbsp;::=&nbsp;"rewrite"&nbsp;proof_list&nbsp;"in"&nbsp;proof</code></div>
 <p>In the formula of the given proof, rewrite according to the equalities
 proved by the specified <a href="#proof-list" target="_self">Proof List</a>, resulting in the
-formula that is proved by this <code class="inline">rewrite</code>-<code class="inline">in</code> statement. In
-particular, for each equality, any term in the formula that is equal
-to the left-hand side of the equality is replaced by the right-hand
-side of the equality.</p>
+formula that is proved by this <code class="inline">rewrite</code>-<code class="inline">in</code> statement. 
+The algorithm for rewriting described in the entry for
+<a href="#rewrite-proof" target="_self">Rewrite (Proof)</a>.</p>
 <div class="code-wrapper"><code id="reference_rewrite_in_example"><!-- Generated by codeUtils.js --></code></div>
 <h2 id="set-type">Set (Type)</h2>
 <p>The <code class="inline">Set&lt;T&gt;</code> type defined in <code class="inline">Set.pf</code> represents the standard