SML basis with type int representing proper integers, not machine words.

Tuned proofs : now use 'algebra ad: ...'

cooper_tac takes now two lists of theorems to be added/deleted from the simpset dor pre-simplification

changed val restriction to local due to smlnj

Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;

Added algebra_tac; tuned;