Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-20 04:48:09 -0700 (Wed, 20 Jun 2001)
Revision: 3279
Log message:

      - Renamed andthenC -> thenC
      - Added byDefT : conv -> tactic
      - Proved rewrites in Itt_dprod
      - Removed some unused stuff from one of the filter_prog interfaces.
      

Changes	Path
+3 -1	metaprl/doc/itt_quickref.txt
+1 -1	metaprl/editor/ml/tests/prop-pigeon.ml
+1 -1	metaprl/filter/base/filter_grammar.ml
+0 -21	metaprl/filter/base/filter_prog.ml
+0 -21	metaprl/filter/base/filter_prog.mli
+8 -8	metaprl/filter/boot/conversionals_boot.ml
+2 -2	metaprl/filter/boot/proof_boot.ml
+2 -2	metaprl/filter/boot/rewrite_boot.ml
+2 -2	metaprl/filter/boot/tactic_boot_sig.mlz
+10 -2	metaprl/theories/base/base_auto_tactic.ml
+1 -0	metaprl/theories/base/base_auto_tactic.mli
+1 -1	metaprl/theories/czf/czf_itt_eq.prla
+1 -1	metaprl/theories/itt/itt_atom_bool.ml
+2 -2	metaprl/theories/itt/itt_bool.ml
+1 -1	metaprl/theories/itt/itt_bool.prla
Added	metaprl/theories/itt/itt_dprod.prla
Properties	metaprl/theories/itt/itt_dprod.prla
+1 -1	metaprl/theories/itt/itt_equal.ml
+1 -1	metaprl/theories/itt/itt_equal.prla
+6 -6	metaprl/theories/itt/itt_int.ml
+5 -5	metaprl/theories/itt/itt_int_base.ml
+3 -3	metaprl/theories/itt/itt_int_base.prla
+3 -3	metaprl/theories/itt/itt_int_bool.ml
+2 -2	metaprl/theories/itt/itt_int_ext.ml
+1 -1	metaprl/theories/itt/itt_int_ext.prla
+1 -1	metaprl/theories/itt/itt_prop_decide.ml
+1 -1	metaprl/theories/itt/itt_prop_decide.prla
+2 -2	metaprl/theories/itt/itt_record.ml
+5 -5	metaprl/theories/itt/itt_record.prla
+1 -1	metaprl/theories/itt/itt_record_exm.prla
+1 -1	metaprl/theories/itt/itt_record_label.ml
+1 -1	metaprl/theories/itt/itt_record_label.prla
+1 -1	metaprl/theories/itt/itt_test.ml
+4 -4	metaprl/theories/tactic/top_conversionals.ml
+1 -1	metaprl/theories/tactic/top_conversionals.mli