helm/www/matita/docs/manual-0.5.9/tac_intros.html

   1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>intros</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets V1.78.1" /><link rel="home" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><link rel="up" href="sec_tactics.html" title="Chapter 7. Tactics" /><link rel="prev" href="tac_intro.html" title="intro" /><link rel="next" href="tac_inversion.html" title="inversion" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">intros</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_intro.html">Prev</a> </td><th width="60%" align="center">Chapter 7. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_inversion.html">Next</a></td></tr></table><hr /></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_intros"></a>intros</h2></div></div></div><p><strong class="userinput"><code>intros hyps</code></strong></p><p>
   3       </p><div class="variablelist"><dl class="variablelist"><dt><span class="term">Synopsis:</span></dt><dd><p><span class="bold"><strong>intros</strong></span> <span class="emphasis"><em><a class="link" href="tacticargs.html#grammar.intros-spec">intros-spec</a></em></span></p></dd><dt><span class="term">Pre-conditions:</span></dt><dd><p>If <span class="command"><strong>hyps</strong></span> specifies a number of hypotheses
   4              to introduce, then the conclusion of the current sequent must
   5              be formed by at least that number of imbricated implications
   6              or universal quantifications.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It applies several times the right introduction rule for
   7              implication, closing the current sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent to prove adding a number of new
   8              hypotheses equal to the number of new hypotheses requested.
   9              If the user does not request a precise number of new hypotheses,
  10              it adds as many hypotheses as possible.
  11              The name of each new hypothesis is either popped from the
  12              user provided list of names, or it is automatically generated when
  13              the list is (or becomes) empty.</p></dd></dl></div><p>
  14     </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_intro.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_inversion.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">intro </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> inversion</td></tr></table></div></body></html>