diff options
| author | Théo Zimmermann | 2020-11-05 11:46:30 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-05 11:46:30 +0100 |
| commit | a5aee12a54f02e84dfc36609f3a61bee36073a39 (patch) | |
| tree | 1d562544517968d3f1ddc436e61cac73a3156682 | |
| parent | 4a22c8332cc562fd65fb96f368c788296eb18bb1 (diff) | |
Add new page to writing proof index.
| -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 |