Summary
- merged
- merged
- tuned proofs -- more explicit use of facts from 'interpret';
- 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);
- tuned;