- (Partial) porting to the new theory with explicit named substitutions

- (Partial) porting to the new theory with explicit named substitutions
- Porting to the new DTD
- Porting to the new query language and to its implementation
- searchPattern implemented: it performs an old "backward" query and then
  tries to apply every result to filter out false matches

Open bugs:
 - ElimIntrosSimpl, Fourier and Ring still to be ported
 - many, many, many others