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.
      

Changes  Path
+5 -1 metaprl/mk/preface
+2 -0 metaprl/refiner/refsig/term_man_sig.ml
+7 -0 metaprl/refiner/term_ds/term_man_ds.ml
+2 -0 metaprl/refiner/term_gen/term_man_gen.ml
+21 -24 metaprl/theories/itt/itt_list.ml
+2988 -2915 metaprl/theories/itt/itt_list.prla
+18 -27 metaprl/theories/itt/itt_unit.ml
Added metaprl/theories/itt/itt_unit.prla
Properties metaprl/theories/itt/itt_unit.prla
+6 -7 metaprl/theories/itt/itt_void.ml
+557 -547 metaprl/theories/itt/itt_void.prla
+3 -0 metaprl/theories/tactic/mptop.ml