1. new syntax for patterns:

1. new syntax for patterns:
    [t] [in p]
   where t is the term to be matched and p is the pattern on the hypotheses
   and on the conclusion (whose syntax is not changed).
   All the tactics now use the new syntax.
2. several tactics have been changed to use the new kind of patterns
   (that also have the optional term in them)
3. the signature of the select function has changed to require the context
   (and return a context and not a "context patch"); moreover it performs
   now both the search for roots and the search for subterms of the roots
   that are alpha-convertible with the optional given term (if any)

WARNING!!!
The following tactics have been commented out for a while:
 replace
 rewrite
 change
 fold