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>DISABLE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>DISABLE</h2>deletes names from current theory
<pre>Major Section: <a href="THEORIES.html">THEORIES</a>
</pre><p>
<pre>
Example:
(disable fact (fact) associativity-of-app)
<p>
General Form:
(disable 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 except 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 ``disable'' a fixed set of names, is:
<pre>
(in-theory (disable name1 name2 ... namek)) ; globally
:in-theory (disable name1 name2 ... namek) ; locally
</pre>
Note that all the names are implicitly quoted. If you wish to
disable a computed list of names, <code>lst</code>, use the theory expression
<code>(set-difference-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>
|
