Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-01 20:54:08 -0700 (Thu, 01 May 2003)
Revision: 4538
Log message:

      - Spelling fixes
      - Moved some of the bind-term+vars manipulation from Perv to Var
      - Added  couple of helper funs in var, used them to simplify a few tactics.
      

Changes	Path
+25 -16	metaprl/library/basic.ml
+1 -1	metaprl/theories/czf/czf_itt_eq.ml
+1 -1	metaprl/theories/czf/czf_itt_equiv.ml
+1 -1	metaprl/theories/czf/czf_itt_nat.ml
+1 -1	metaprl/theories/czf/czf_itt_set.ml
+1 -1	metaprl/theories/czf/czf_itt_set_ind.ml
+2 -24	metaprl/theories/itt/itt_bool.ml
+1 -1	metaprl/theories/itt/itt_derive.ml
+1 -0	metaprl/theories/itt/itt_grouplikeobj.ml
+11 -13	metaprl/theories/itt/itt_int_base.ml
+2 -14	metaprl/theories/itt/itt_nat.ml
+6 -21	metaprl/theories/itt/itt_relation_str.ml
+2 -25	metaprl/theories/itt/itt_squiggle.ml
+3 -23	metaprl/theories/itt/itt_struct.ml
+5 -34	metaprl/theories/itt/itt_struct2.ml
+1 -0	metaprl/theories/tactic/mptop.ml
+0 -9	metaprl/theories/tactic/perv.ml
+0 -2	metaprl/theories/tactic/perv.mli
+1 -1	metaprl/theories/tactic/top_tacticals.ml
+29 -12	metaprl/theories/tactic/var.ml
+7 -3	metaprl/theories/tactic/var.mli