Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-16 08:08:15 -0800 (Tue, 16 Nov 1999)
Revision: 2852
Log message:
Fixed some problems with TPTP.
create_tptp is still disabled in editor/ml/shell.ml,
so z.ml still does not work.