Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-28 00:48:10 -0700 (Mon, 28 Jul 2003)
Revision: 4780
Log message:
- Now one can use withT to tell JProver with term to use as a canonical
element of types (JProver presumes all types to be non-empty) instead
of the default << 'v0_jprover >>.
- Killed some of the debugging printouts in JProver.
Changes | Path |
+19 -19 | metaprl/refiner/reflib/jall.ml |
+2 -1 | metaprl/theories/itt/itt_logic.ml |
+20 -20 | metaprl/theories/itt/jprover_tests.ml |
+360 -358 | metaprl/theories/itt/jprover_tests.prla |