Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-12-29 15:30:21 -0800 (Tue, 29 Dec 1998)
Revision: 2529
Log message:

      Added pigeonhole problem in editor/ml/test.ml.
      
      To try it:
      
      % ./mptop
      # #use "y.ml";;
      # refine timingT proveT;;
      

Changes	Path
+1 -0	metaprl/editor/ml/Makefile
+112 -20	metaprl/editor/ml/test.ml
+1 -1	metaprl/editor/ml/test.mli
+3 -29	metaprl/editor/ml/y.ml
+8 -8	metaprl/filter/term_grammar.ml
+5 -3	metaprl/theories/itt/itt_logic.ml
+1 -0	metaprl/theories/itt/itt_logic.mli
+31 -34	metaprl/theories/itt/itt_prop_decide.ml
+5 -5	metaprl/theories/itt/itt_prop_decide.mli
+1 -1	metaprl/theories/itt/itt_theory.ml