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
|
<html>
<head><title>DEFTHMD.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>DEFTHMD</h2>prove and name a theorem and then disable it
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<p>
Use <code>defthmd</code> instead of <code><a href="DEFTHM.html">defthm</a></code> when you want to disable a theorem
immediately after proving it. This macro has been provided for users who
prefer working in a mode where theorems are only enabled when explicitly
directed by <code>:</code><code><a href="IN-THEORY.html">in-theory</a></code>. Specifically, the form
<pre>
(defthmd NAME TERM ...)
</pre>
expands to:
<pre>
(progn
(defthmd NAME TERM ...)
(with-output
:off summary
(in-theory (disable NAME)))
(value NAME)).
</pre>
<p>
Note that <code>defthmd</code> commands are never redundant (see <a href="REDUNDANT-EVENTS.html">redundant-events</a>).
Even if the <code>defthm</code> event is redundant, then the <code><a href="IN-THEORY.html">in-theory</a></code> event
will still be executed.<p>
The summary for the <code><a href="IN-THEORY.html">in-theory</a></code> event is suppressed. See <a href="DEFTHM.html">defthm</a> for
documentation of <code>defthm</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>
|
