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
|
<html>
<head><title>ACL2-PC_colon__colon_REMOVE-ABBREVIATIONS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>ACL2-PC::REMOVE-ABBREVIATIONS</h3>(primitive)
<code> </code>remove one or more abbreviations
<pre>Major Section: <a href="PROOF-CHECKER-COMMANDS.html">PROOF-CHECKER-COMMANDS</a>
</pre><p>
<pre>
Examples:
remove-abbreviations -- remove all abbreviations
(remove-abbreviations v w)
-- assuming that V and W currently abbreviate
terms, then they are ``removed'' in the
sense that they are no longer considered to
abbreviate those terms
<p>
General Forms:
(remove-abbreviations &rest vars)
</pre>
If vars is not empty (i.e., not <code>nil</code>), remove the variables in <code>vars</code>
from the current list of abbreviations, in the sense that each
variable in <code>vars</code> will no longer abbreviate a term.<p>
<strong>Note:</strong> The instruction fails if at least one of the arguments
fails to be a variable that abbreviates a term.<p>
See also the documentation for <code>add-abbreviation</code>, which contains a
discussion of abbreviations in general, and <code>show-abbreviations</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>
|
