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
|
<html>
<head><title>IN-PACKAGE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>IN-PACKAGE</h2>select current package
<pre>Major Section: <a href="OTHER.html">OTHER</a>
</pre><p>
<pre>
Example:
(in-package "MY-PKG")
<p>
General Form:
(in-package str)
</pre>
where <code>str</code> is a string that names an existing ACL2 package, i.e.,
one of the initial packages such as <code>"KEYWORD"</code> or <code>"ACL2"</code> or a
package introduced with <code><a href="DEFPKG.html">defpkg</a></code>. For a complete list of the known
packages created with <code><a href="DEFPKG.html">defpkg</a></code>, evaluate
<pre>
(strip-cars (known-package-alist state)).
</pre>
See <a href="DEFPKG.html">defpkg</a>. An ACL2 book (see <a href="BOOKS.html">books</a>) must contain a single <code>in-package</code>
form, which must be the first form in that book.
<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>
|
