Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-17 20:30:36 -0800 (Thu, 17 Feb 2000)
Revision: 2890
Log message:

      Restored the old code for proving the propositional pigeon-hole principle.
      For some reason the proveT tactic does not get exported properly,
      so p4.ml still does not work.
      

Changes	Path
+1 -1	metaprl/editor/ml/tests/p4.ml
+351 -1	metaprl/editor/ml/tests/prop-pigeon.ml
+42 -0	metaprl/editor/ml/tests/prop-pigeon.mli
+3 -0	metaprl/mk/preface