Added lemmas to Ring_and_Field with slightly modified simplification rules
Deleted some little-used integer theorems, replacing them by the generic ones
in Ring_and_Field
Consolidated integer powers
use "../settings";
use_thy "termination";
use_thy "Induction";
use_thy "Nested1";
use_thy "Nested2";