This reverts commit c3b4196fd737315a9328f5729c839a18f709b471.

The relevant hash-tables are weak both in keys and values

encoding_enumeration add projection for enumerated type. Seems to work (on valid and not valid goal) for simplify, spass, eprover

see examples/programs/sorted_list.mlw with eprover, spass, simplify!!

encoding_enumeration must be used with encoding_decorate and encoding_instantiate if an enumeration type is kept.

This allows to have one line less in transformations.

with a different logic of splitting in premises - to discuss.
Its main advantage is providing two transformations instead of 6.

a meta of an exclusive kind removes the previous meta of this 
kind (if any) from task_meta.

Discuss: should driver-imposed exclusive metas have a low priority
(i.e. driver does not add an exclusive meta if the task already 
contains one of this kind) or should we just trust the driver
authors not to put exclusive metas in drivers? 

- bring driver syntax closer to that of theories
- some simple API improvements

Since its already incorrect no encoding for simplify, and also no trigger because its buggy inside simplify

- everything is converted to the new shiny way of doing things.
  Well, everything except Gappa, which seems very unifinished anyway,
  and Encoding_instantiate, which is too complex and would like to 
  update it with François.

Also, I commented a little piece of exception reporting in manager/,
will see it with Claude.

THIS IS STILL A WORK IN PROGRESS!
Please inform me about any bugs, ugly APIs, and proposed corrections.

All the non-implemented things, mentioned in the previous commit
message are still in the TODO list and will be done soon.

- dependent transformations (ones that depend on cloning history
  and/or metaproperties) have now the same type Trans.trans and
  can be registered via Trans, too.
- load_driver accumulates appropriate tdecls to be appended to
  tasks before transformation/printing.

At this moment, we have almost everything in place and are ready
to remove Register module (subsumed by Trans and Printer in core/)
and Prover module (its functions will move to Driver), and convert
all printers and transformations to use the new infrastructure. 

Not implemented yet:
- appending driver-imposed tdecls to tasks - when and where?
- metas-options - what is the best way to implement them?
- syntax/typing for metas in theories and drivers.

completion : complete theories and goals