diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 83b8bc2308..a7eb7c2319 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1179,10 +1179,10 @@ Printing |Ltac| tactics Examples of using |Ltac| ------------------------- -About the cardinality of the set of natural numbers -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Proof that the natural numbers have at least two elements +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. example:: About the cardinality of the set of natural numbers +.. example:: Proof that the natural numbers have at least two elements The first example shows how to use pattern matching over the proof context to prove that natural numbers have at least two |