Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-31 07:35:45 -0700 (Fri, 31 Jul 1998)
Revision: 2376
Log message:

      Added TPTP theory, and Ensemble library.  Fixed sequent displays.
      BUG: rewrites fail on sequents.
      

Changes	Path
+1 -1	metaprl/Makefile
Properties	metaprl/doc
+1 -1	metaprl/editor/emacs/caml.el
Added	metaprl/editor/ml/GEN.p
Properties	metaprl/editor/ml/GEN.p
+11 -8	metaprl/editor/ml/Makefile
Added	metaprl/editor/ml/czf.ml
Properties	metaprl/editor/ml/czf.ml
+7 -3	metaprl/editor/ml/nl
+2 -0	metaprl/editor/ml/nl.ml
+1 -0	metaprl/editor/ml/nl.mli
Added	metaprl/editor/ml/nlopt
Properties	metaprl/editor/ml/nlopt
+24 -28	metaprl/editor/ml/package_info.ml
+11 -2	metaprl/editor/ml/shell.ml
+1 -0	metaprl/editor/ml/shell.mli
+66 -26	metaprl/editor/ml/shell_nl.ml
+9 -2	metaprl/editor/ml/shell_p4.ml
+5 -0	metaprl/editor/ml/shell_p4.mli
+19 -14	metaprl/editor/ml/shell_rule.ml
+10 -16	metaprl/editor/ml/y.ml
Added	metaprl/editor/ml/z.ml
Properties	metaprl/editor/ml/z.ml
Properties	metaprl/ensemble
Added	metaprl/ensemble/Makefile
Properties	metaprl/ensemble/Makefile
Added	metaprl/ensemble/nlapp.ml
Properties	metaprl/ensemble/nlapp.ml
Added	metaprl/ensemble/nlapp.mli
Properties	metaprl/ensemble/nlapp.mli
+4 -2	metaprl/filter/filter_cache_fun.ml
+2 -2	metaprl/filter/filter_summary.ml
+13 -7	metaprl/mk/config
+18 -14	metaprl/mllib/list_util.ml
+176 -161	metaprl/mllib/splay_set.ml
+16 -2	metaprl/mllib/splay_set.mli
+0 -13	metaprl/refiner/refbase/opname.ml
+0 -1	metaprl/refiner/refbase/opname.mli
+5 -1	metaprl/refiner/refiner/rewrite.mlp
+15 -1	metaprl/refiner/reflib/dform.ml
+12 -3	metaprl/refiner/reflib/term_table.ml
+3 -0	metaprl/refiner/refsig/term_op_sig.ml
+1 -0	metaprl/refiner/refsig/term_shape_sig.ml
+25 -0	metaprl/refiner/term_ds/term_op_ds.mlp
+1 -1	metaprl/refiner/term_gen/term_man_gen.mlp
+28 -20	metaprl/refiner/term_gen/term_shape_gen.mlp
+39 -0	metaprl/refiner/term_std/term_op_std.mlp
Added	metaprl/script
Properties	metaprl/script
+7 -6	metaprl/theories/base/base_dform.ml
+0 -1	metaprl/theories/itt/Makefile
+18 -1	metaprl/theories/itt/itt_atom.ml
+4 -0	metaprl/theories/itt/itt_atom.mli
+4 -0	metaprl/theories/itt/itt_dprod.ml
+2 -2	metaprl/theories/itt/itt_fun.ml
+2 -2	metaprl/theories/itt/itt_list.ml
+393 -38	metaprl/theories/itt/itt_logic.ml
+5 -18	metaprl/theories/itt/itt_logic.mli
Binary	metaprl/theories/itt/itt_logic.prlb
Properties	metaprl/theories/itt/itt_logic.prlb
+2 -0	metaprl/theories/itt/itt_prod.ml
Deleted	metaprl/theories/itt/itt_soft.ml
Deleted	metaprl/theories/itt/itt_soft.mli
+12 -7	metaprl/theories/itt/itt_union.ml
+1 -0	metaprl/theories/itt/itt_union.mli
Properties	metaprl/theories/tactic
+6 -0	metaprl/theories/tactic/Makefile
+1 -1	metaprl/theories/tactic/perv.ml
+1 -1	metaprl/theories/tactic/perv.mli
Added	metaprl/theories/tactic/remote_refiner.ml
Properties	metaprl/theories/tactic/remote_refiner.ml
Added	metaprl/theories/tactic/remote_refiner.mli
Properties	metaprl/theories/tactic/remote_refiner.mli
+80 -294	metaprl/theories/tactic/tactic_type.ml
Added	metaprl/theories/tactic/thread_refiner_null.ml
Properties	metaprl/theories/tactic/thread_refiner_null.ml
Added	metaprl/theories/tactic/thread_refiner_null.mli
Properties	metaprl/theories/tactic/thread_refiner_null.mli
Added	metaprl/theories/tactic/thread_refiner_sig.mlz
Properties	metaprl/theories/tactic/thread_refiner_sig.mlz
Added	metaprl/theories/tactic/thread_refiner_tree.ml
Properties	metaprl/theories/tactic/thread_refiner_tree.ml
Added	metaprl/theories/tactic/thread_refiner_tree.mli
Properties	metaprl/theories/tactic/thread_refiner_tree.mli
Properties	metaprl/theories/tptp
Added	metaprl/theories/tptp/Makefile
Properties	metaprl/theories/tptp/Makefile
Added	metaprl/theories/tptp/tptp.ml
Properties	metaprl/theories/tptp/tptp.ml
Added	metaprl/theories/tptp/tptp.mli
Properties	metaprl/theories/tptp/tptp.mli
Binary	metaprl/theories/tptp/tptp.prlb
Properties	metaprl/theories/tptp/tptp.prlb
Added	metaprl/theories/tptp/tptp_lex.mli
Properties	metaprl/theories/tptp/tptp_lex.mli
Added	metaprl/theories/tptp/tptp_lex.mll
Properties	metaprl/theories/tptp/tptp_lex.mll
Added	metaprl/theories/tptp/tptp_load.ml
Properties	metaprl/theories/tptp/tptp_load.ml
Added	metaprl/theories/tptp/tptp_load.mli
Properties	metaprl/theories/tptp/tptp_load.mli
Added	metaprl/theories/tptp/tptp_parse.mly
Properties	metaprl/theories/tptp/tptp_parse.mly
Added	metaprl/theories/tptp/tptp_prove.ml
Properties	metaprl/theories/tptp/tptp_prove.ml
Added	metaprl/theories/tptp/tptp_prove.mli
Properties	metaprl/theories/tptp/tptp_prove.mli
Added	metaprl/theories/tptp/tptp_type.mlz
Properties	metaprl/theories/tptp/tptp_type.mlz