Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-17 07:10:39 -0700 (Sun, 17 Jun 2001)
Revision: 3272
Log message:

      Wrote Itt_struct.nthAssumT that is very similar to base theory nthAssumT, but
      can also do thinning. I added it to trivialT, so now trivialT and autoT can
      do thinning when matching the goal against assumptions.
      

Changes	Path
+4 -0	metaprl/doc/itt_quickref.txt
+42 -22	metaprl/refiner/reflib/match_seq.ml
+13 -7	metaprl/refiner/reflib/match_seq.mli
+2 -2	metaprl/theories/itt/ctt_markov.prla
+7 -7	metaprl/theories/itt/itt_bool.prla
+1 -1	metaprl/theories/itt/itt_bunion.prla
+12 -12	metaprl/theories/itt/itt_collection.prla
+3 -3	metaprl/theories/itt/itt_dfun.prla
+3 -3	metaprl/theories/itt/itt_dprod_imp.prla
+1 -1	metaprl/theories/itt/itt_esquash.prla
+18 -18	metaprl/theories/itt/itt_fset.prla
+1 -1	metaprl/theories/itt/itt_fun.prla
+2 -2	metaprl/theories/itt/itt_isect.prla
+1 -1	metaprl/theories/itt/itt_list.prla
+3 -3	metaprl/theories/itt/itt_logic.prla
+5 -5	metaprl/theories/itt/itt_nat.prla
+1 -1	metaprl/theories/itt/itt_prod.prla
+6 -6	metaprl/theories/itt/itt_record0.prla
+2 -2	metaprl/theories/itt/itt_record_label0.prla
+2 -2	metaprl/theories/itt/itt_rfun.prla
+1 -1	metaprl/theories/itt/itt_squash.prla
+25 -2	metaprl/theories/itt/itt_struct.ml
+3 -2	metaprl/theories/itt/itt_struct.mli
+1 -1	metaprl/theories/itt/itt_struct2.prla
+3 -3	metaprl/theories/itt/itt_struct3.prla