diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/auto.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/index.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/logic.rst | 5 |
3 files changed, 8 insertions, 4 deletions
diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index 961af65b86..cc8af976d2 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -1,7 +1,8 @@ .. _automation: -Automation ----------- +========================= +Programmable proof search +========================= .. tacn:: auto :name: auto diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst index a219770c69..fa0b0e51af 100644 --- a/doc/sphinx/proofs/automatic-tactics/index.rst +++ b/doc/sphinx/proofs/automatic-tactics/index.rst @@ -13,8 +13,10 @@ complex goals in new domains. .. toctree:: :maxdepth: 1 + logic ../../addendum/omega ../../addendum/micromega ../../addendum/ring ../../addendum/nsatz + auto ../../addendum/generalized-rewriting diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst index 1312c25f63..acf64ae437 100644 --- a/doc/sphinx/proofs/automatic-tactics/logic.rst +++ b/doc/sphinx/proofs/automatic-tactics/logic.rst @@ -1,7 +1,8 @@ .. _decisionprocedures: -Decision procedures -------------------- +============================== +Solvers for logic and equality +============================== .. tacn:: tauto :name: tauto |