Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-25 00:00:19 -0800 (Sat, 25 Jan 2003)
Revision: 4022
Log message:

      Split nth_nyp into two functions: nth_hyp and nth_binding.
      

Changes	Path
+2 -2	metaprl/filter/boot/sequent_boot.ml
+2 -2	metaprl/filter/boot/tactic_boot.ml
+4 -2	metaprl/filter/boot/tactic_boot_sig.mlz
+1 -1	metaprl/filter/boot/tacticals_boot.ml
+1 -1	metaprl/refiner/reflib/arith.ml
+2 -1	metaprl/refiner/refsig/term_man_sig.ml
+20 -2	metaprl/refiner/term_ds/term_man_ds.ml
+22 -1	metaprl/refiner/term_gen/term_man_gen.ml
+6 -6	metaprl/theories/base/base_dtactic.ml
+2 -2	metaprl/theories/czf/czf_itt_eq.ml
+3 -3	metaprl/theories/czf/czf_itt_equiv.ml
+1 -1	metaprl/theories/czf/czf_itt_set.ml
+1 -1	metaprl/theories/fol/fol_prop.ml
+2 -3	metaprl/theories/fol/fol_struct.ml
+1 -1	metaprl/theories/itt/itt_bisect.ml
+2 -4	metaprl/theories/itt/itt_bool.ml
+2 -5	metaprl/theories/itt/itt_derive.ml
+1 -1	metaprl/theories/itt/itt_disect.ml
+1 -1	metaprl/theories/itt/itt_equal.ml
+1 -1	metaprl/theories/itt/itt_fun.ml
+4 -9	metaprl/theories/itt/itt_int_arith.ml
+2 -1	metaprl/theories/itt/itt_int_base.ml
+1 -1	metaprl/theories/itt/itt_isect.ml
+11 -16	metaprl/theories/itt/itt_logic.ml
+1 -1	metaprl/theories/itt/itt_prop_decide.ml
+1 -1	metaprl/theories/itt/itt_squash.ml
+1 -2	metaprl/theories/itt/itt_squiggle.ml
+4 -6	metaprl/theories/itt/itt_struct.ml
+3 -5	metaprl/theories/itt/itt_struct2.ml
+1 -2	metaprl/theories/itt/itt_subtype.ml
+5 -5	metaprl/theories/tptp/tptp_prove.ml