Changes

Summary

1. merged
2. merged
3. tuned proofs -- more explicit use of facts from 'interpret';
4. replaced vacuous class nat_int/real_int by more elementary locale + interpretation: this avoids implicit sort constraints imposed on theorems, as well as pointless dictionary constructions (foo_dict);
5. tuned;