Simplifies a theorem, using the theorem’s assumptions as rewrites in
addition to the provided rewrite theorems and simpset.
LIBRARY
simpLib
FAILURE
Never fails, but may diverge.
EXAMPLE
- ASM_SIMP_RULE bool_ss [] (ASSUME (Term `x = 3`))
> val it = [.] |- T : thm
USES
The assumptions can be used to simplify the conclusion of the theorem.
For example, if the conclusion of a theorem is an implication, the
antecedent together with the hypotheses may help simplify the conclusion.