1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
<html>
<head><title>ENABLE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ENABLE</h2>adds names to current theory
<pre>Major Section: <a href="THEORIES.html">THEORIES</a>
</pre><p>
<pre>
Example:
(enable fact (fact) associativity-of-app)
<p>
General Form:
(enable name1 name2 ... namek)
</pre>
where each <code>namei</code> is a runic designator; see <a href="THEORIES.html">theories</a>. The
result is the theory that contains all the names in the current
theory plus those listed. Note that this is merely a function that
returns a theory. The result is generally a very long list of <a href="RUNE.html">rune</a>s
and you will probably regret printing it.<p>
The standard way to ``enable'' a fixed set of names, is
<pre>
(in-theory (enable name1 name2 ... namek)) ; globally
:in-theory (enable name1 name2 ... namek) ; locally
</pre>
Note that all the names are implicitly quoted. If you wish to
enable a computed list of names, <code>lst</code>, use the theory expression
<code>(union-theories (current-theory :here) lst)</code>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
