add_implicit_rewrites
Rewrite.add_implicit_rewrites: thm list -> unit
Augments the built-in database of simplifications automatically included in rewriting.
Used to build up the power of the built-in simplification set.
Press ← or → to navigate between chapters
Press S or / to search in the book
Press ? to show this help
Press Esc to hide this help
add_implicit_rewritesRewrite.add_implicit_rewrites: thm list -> unit
Augments the built-in database of simplifications automatically included in rewriting.
Used to build up the power of the built-in simplification set.