Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-23 07:02:37 -0800 (Sun, 23 Mar 2003)
Revision: 4220
Log message:
*** WARNING ***
*** This breaks prlb compatibility again! ***
- I got rid of the variable arguments to rules and rewrites. Now the rewriter
handles all the variable naming internally.
- All the maybe_new_vars1 - maybe_new_vars9 functions are gone. When creating
a bind term by var_subst, instead of creating a new variable for it, call
Perv.var_subst_to_bind
- To rename a variable in a hypothesis, use the nameHypT tactic - it
now can handle both binding and binding-free hyps.