rule.html 681 Bytes
Newer Older
Sarah Grebing's avatar
Sarah Grebing committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
<!DOCTYPE html>
<html lang="en">
<head>
    <meta charset="UTF-8">
    <title>rule</title>
</head>
<body>
<h2 id="rule">Rule Application</h2>
<blockquote>
    <p>Synopsis: <code>rule tacletname on=&lt;TERM&gt; formula=&lt;TERM&gt; occ=&lt;INT&gt; </code></p>
</blockquote>
Rule keyword can be ommited
<p><strong>Arguments:</strong></p>
<ul>
    <li>rulename : <em>STRING</em> name of taclet to apply</li>
    <li><code>on</code> : <em>TERM</em> (find term of the taclet)</li>
    <li><code>formula</code>: <em>TERM</em> (top-level formula in which term appears)</li>
    <li><code>occ</code> : <em>INT</em> (occurrence number of term formula in sequent)</li>
</ul>
</body>
</html>