Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-15 19:51:15 -0800 (Sat, 15 Jan 2005)
Revision: 6408
Log message:

      Added the conversion "findThenC test conv" that find the outermost
      subterms where test is true, and applies the conv.
      

Changes	Path
+17 -8	metaprl/refiner/rewrite/rewrite_match_redex.ml
+4 -0	metaprl/support/tactics/top_conversionals.ml
+1 -0	metaprl/support/tactics/top_conversionals.mli
+22 -4	metaprl/tactics/proof/conversionals_boot.ml
+5 -0	metaprl/tactics/proof/tactic_boot_sig.ml
Properties	metaprl/theories