Lemma Collections

The default setup of the simplifier and other automatic proof methods in Isabelle includes lemmas which are considered generally useful and (almost) never make a goal harder to prove (or unprovable). Apart from this default setup, Isabelle offers some collections of lemmas that are useful to prove specific kinds of goals:

Collection Usage
eval_nat_numeral simp rules to convert numerals to Suc/Zero notation
ac_simps TODO
algebra_simps simp rules to deal with the classical algebraic structures of groups and rings and fields. They simplify terms by multiplying everything out (in case of a ring) and bringing sums and products into a canonical form (by ordered rewriting). As a result, it decides group and ring equalities but also helps with inequalities.

Of course it also works for fields, but it knows nothing about multiplicative inverses or division. This is catered for by field_simps.

field_simps simp rules that multiply with denominators in (in)equations if they can be proved to be non-zero (for equations) or positive/negative (for inequations); can be too aggressive and is therefore separate from the more benign algebra_simps.
sign_simps TODO
tendsto_intros TODO