changed auto_tac params type and all derivate tactics like applyS and

demodulate honors the same syntax.

new syntax for auto parameters:
  auto string-params by only_terms_to_use
new syntax for declarative eq chains:
  [(conclude|obtain H) t1] = t2 (auto-params|exact t|using t|proof)
  exact t : apply t
  using t : 1 demodulation step using t
  auto-params : first [ auto ; auto paramodulation ]
  proof : id_tac
manual still to be updated