Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-12 23:16:19 -0700 (Mon, 12 Jun 2000)
Revision: 3014
Log message:
I wrote a proof tree normalization that tries to eliminate unnecessary nodes
in the proof tree and makes "deep" proof browsing much more
plesent.
Currently this is probably a little inefficient since it' too eager and
the results are not always saved. To fix this, we'll need to make Tactic_boot extracts
mutable so that we could do normalization (and other operations) properly lazily.
Other small changes.