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, which are useful to prove specific kinds of goals.

Collection	Usage
eval_nat_numeral	simp rules to convert numerals to Suc/Zero notation
algebra_simps	The rules deal with the classical algebraic structures of groups, rings and family. 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	These rules 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
DERIV_intros
tendsto_intros
ac_simps	associativity and commutativity simplification rules