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
|
<html>
<head><title>CHECKPOINT-FORCED-GOALS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>CHECKPOINT-FORCED-GOALS</h2>Cause forcing goals to be checkpointed in proof trees
<pre>Major Section: <a href="PROOF-TREE.html">PROOF-TREE</a>
</pre><p>
<pre>
Example forms:
(checkpoint-forced-goals t)
(checkpoint-forced-goals nil)
</pre>
Also see <a href="PROOF-TREE.html">proof-tree</a>.
<p>
By default, goals are not marked as checkpoints by a proof tree
display (as described elsewhere; see <a href="PROOF-TREE.html">proof-tree</a>)
merely because they <a href="FORCE.html">force</a> some hypotheses, thus possibly
contributing to a forcing round. However, some users may want such
behavior, which will occur once the command <code>(checkpoint-forced-goals</code>
<code>t</code>) has been executed. To return to the default behavior, use the
command <code>(checkpoint-forced-goals nil)</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>
|
