Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-12 19:40:43 -0800 (Thu, 12 Feb 2004)
Revision: 5370
Log message:

      Top_conversionals.apply_rewrite should use tactic_arg, not bookmark as an input.
      

Changes  Path
+2 -1 metaprl/filter/phobos/phobos_rewrite.ml
+2 -2 metaprl/support/tactics/top_conversionals.ml
+1 -1 metaprl/support/tactics/top_conversionals.mli
+0 -1 metaprl/tactics/proof/rewrite_boot.ml
+3 -3 metaprl/tactics/proof/tactic_boot_sig.ml