Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2000-10-03 14:15:35 -0700 (Tue, 03 Oct 2000)
Revision: 3080
Log message:
small bug in timestamps; fixed.
| Changes | Path |
| +12 -12 | metaprl/refiner/term_ds/term_unif_ds.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2000-10-06 10:17:39 -0700 (Fri, 06 Oct 2000)
Revision: 3081
Log message:
some documenting markup and resource annotation added
| Changes | Path |
| +208 -29 | metaprl/theories/itt/itt_int_base.ml |
| +39 -7 | metaprl/theories/itt/itt_int_base.mli |
| +87 -25 | metaprl/theories/itt/itt_int_ext.ml |
| +36 -4 | metaprl/theories/itt/itt_int_ext.mli |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-10-08 09:38:54 -0700 (Sun, 08 Oct 2000)
Revision: 3082
Log message:
Fixed the problem with leftward-moving margins, for example:
pushm[5] pushm[3]
The choice I made is similar to Carl's recommendation.
If the offset is negative, the current margin string is
always truncated and replaced with the new margin string.
However, an error message is printed if the overlap does not
match.
| Changes | Path |
| +43 -2 | metaprl/refiner/reflib/rformat.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2000-10-10 05:29:43 -0700 (Tue, 10 Oct 2000)
Revision: 3083
Log message:
reduce_resources added and theories added to Makefile
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2000-10-10 22:28:11 -0700 (Tue, 10 Oct 2000)
Revision: 3084
Log message:
A couple of rewrites turn from primitive to interative
| Changes | Path |
| +4 -0 | metaprl/theories/itt/itt_int_base.ml |
| +3 -0 | metaprl/theories/itt/itt_int_base.mli |
| +2 -2 | metaprl/theories/itt/itt_int_ext.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-10-18 14:32:01 -0700 (Wed, 18 Oct 2000)
Revision: 3085
Log message:
Fixed Yegor's typos that prevented MetaPRL from staring (Yegor, please
take a look at my changes)
Other minor fixes.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-10-22 13:58:58 -0700 (Sun, 22 Oct 2000)
Revision: 3086
Log message:
1) Proved some *Formation rules that used to be primitive (using in part
Alexei's cut rule idea). We should probably continue this job and
eliminate "primitiveness" from as much Formation rules as we can.
2) unitSqequal rule should be primitive
3) mk: don't pass -j1 to make when MAKE_JOBS = 1
4) In MP toploop, when a non-negatice integer is found where
an address was expected, that integer is considered to be
the hypothesis number. This enables applying primitive rules
from the MP toploop.