diff options
| author | Théo Zimmermann | 2020-11-05 12:50:43 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-05 14:23:27 +0100 |
| commit | d517069251fe86469c46984503805e95e837c737 (patch) | |
| tree | 771093ee737bd41c7f271651fa550e80dfaa33b1 | |
| parent | b6f3e7696ec73cb919343d54dcfe9f62a787be54 (diff) | |
Add new sections to automatic tactic chapter.
| -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 |