diff options
| author | Clément Pit-Claudel | 2020-03-19 18:42:10 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-03-19 18:42:10 -0400 |
| commit | 47d92a69773755e2ad5d5f987f87337fdf7e98d8 (patch) | |
| tree | 3a074b1269952ef2cbbb4d5fce64531580c61443 /doc/sphinx/proofs/automatic-tactics | |
| parent | 9f680f776140c8b3b8f79013262d5bd73761d571 (diff) | |
| parent | 1be31dea4cfd31522898edc07fee0829fea7c68d (diff) | |
Merge PR #11601: [refman] Move chapters into new structure.
Reviewed-by: jfehrle
Diffstat (limited to 'doc/sphinx/proofs/automatic-tactics')
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/index.rst | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst new file mode 100644 index 0000000000..a219770c69 --- /dev/null +++ b/doc/sphinx/proofs/automatic-tactics/index.rst @@ -0,0 +1,20 @@ +.. _automatic-tactics: + +===================================================== +Built-in decision procedures and programmable tactics +===================================================== + +Some tactics are largely automated and are able to solve complex +goals. This chapter presents both some decision procedures that can +be used to solve some specific categories of goals, and some +programmable tactics, that the user can instrument to handle some +complex goals in new domains. + +.. toctree:: + :maxdepth: 1 + + ../../addendum/omega + ../../addendum/micromega + ../../addendum/ring + ../../addendum/nsatz + ../../addendum/generalized-rewriting |