Major Section: MISCELLANEOUS
Example Input File for Rebuild: (defun fn1 (x y) ...) (defthm lemma1 ...) (defthm lemma2 ...) (i-am-here) The following lemma won't go through. I started typing the hint but realized I need to prove a lemma first. See the failed proof attempt in foo.bar. I'm going to quit for the night now and resume tomorrow from home.
(defthm lemma3 ... :hints (("Goal" :use (:instance ??? ...
By putting an
(i-am-here) form at the ``frontier'' of an evolving
file of commands, you can use
rebuild to load the file up to the
I-am-here simply returns an
ld error triple and any
form that ``causes an error'' will do the same job. Note that the
text of the file after the
(i-am-here) need not be machine