diff options
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/index.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 4 |
2 files changed, 5 insertions, 0 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst index 3f5526dba8..ebd75ef300 100644 --- a/doc/sphinx/proofs/writing-proofs/index.rst +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -29,6 +29,7 @@ flavors of tactics, including the SSReflect proof language. ../../proof-engine/proof-handling ../../proof-engine/tactics + rewriting ../../proof-engine/ssreflect-proof-language ../../proof-engine/detailed-tactic-examples ../../user-extensions/proof-schemes diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 411eddff42..040849a9ef 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -1,3 +1,7 @@ +================================= +Term rewriting and simplification +================================= + .. _rewritingexpressions: Rewriting expressions |