</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It adds to the context of the current sequent to prove a new
definition <span><strong class="command">x ≝ t</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_left.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_normalize.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">left </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> normalize <pattern></td></tr></table></div></body></html>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It adds to the context of the current sequent to prove a new
definition <span><strong class="command">x ≝ t</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_left.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_normalize.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">left </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> normalize <pattern></td></tr></table></div></body></html>