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
36
37
38
39
40
41
42
43
|
<html>
<head><title>IN-THEORY.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>IN-THEORY</h2>designate ``current'' theory (enabling its rules)
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Example:
(in-theory (set-difference-theories
(universal-theory :here)
'(flatten (:executable-counterpart flatten))))
<p>
General Form:
(in-theory term :doc doc-string)
</pre>
where <code>term</code> is a term that when evaluated will produce a theory
(see <a href="THEORIES.html">theories</a>), and <code><a href="DOC-STRING.html">doc-string</a></code> is an optional <a href="DOCUMENTATION.html">documentation</a>
string not beginning with ``<code>:doc-section</code> ...''. Except for the
variable <code><a href="WORLD.html">world</a></code>, <code>term</code> must contain no free variables. <code>Term</code> is
evaluated with the variable <code><a href="WORLD.html">world</a></code> bound to the current <a href="WORLD.html">world</a> to
obtain a theory and the corresponding runic theory
(see <a href="THEORIES.html">theories</a>) is then made the current theory. Thus,
immediately after the <code>in-theory</code>, a rule is <a href="ENABLE.html">enable</a>d iff its rule name
is a member of the runic interpretation (see <a href="THEORIES.html">theories</a>) of some
member of the value of <code>term</code>. See <a href="THEORY-FUNCTIONS.html">theory-functions</a> for a list
of the commonly used theory manipulation functions.<p>
Because no unique name is associated with an <code>in-theory</code> event, there
is no way we can store the <a href="DOCUMENTATION.html">documentation</a> string <code><a href="DOC-STRING.html">doc-string</a></code> in our
<a href="DOCUMENTATION.html">documentation</a> data base. Hence, we actually prohibit <code><a href="DOC-STRING.html">doc-string</a></code>
from having the form of an ACL2 <a href="DOCUMENTATION.html">documentation</a> string;
see <a href="DOC-STRING.html">doc-string</a>.<p>
Also see <a href="HINTS.html">hints</a> for a discussion of the <code>:in-theory</code> hint, including some
explanation of the important point that an <code>:in-theory</code> hint will always be
evaluated relative to the current ACL2 logical <a href="WORLD.html">world</a>, not relative to
the theory of a previous goal.
<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>
|
