The default theory of +, -, *, /, and EXPT for the IHS library.
This theory simply consists of the theories integerp-algebra
This theory is the default theory exported by the ihs/math-lemmas book.
This theory will normally be ENABLEd by every book in the IHS library.
- A theory of EXPT which is compatible with the ALGEBRA theories.
- A basic theory of algebra for all INTEGERPs.