diff options
| author | Théo Zimmermann | 2018-10-24 14:38:42 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-24 14:38:42 +0200 |
| commit | d1318fa71c4a65693dce14fa04d203d0b571eb25 (patch) | |
| tree | 9b6fd17022d37be38880f4a5b1c4f195e0f3a57e | |
| parent | 3dd46db42776f9be448454b2ddf556663295abd8 (diff) | |
| parent | 5fb1677a4bf62155ef0f57c0a0b189d42e05505f (diff) | |
Merge PR #8776: Replace non-idiomatic "dead-alleys" with idiomatic "dead-ends"
| -rw-r--r-- | doc/sphinx/credits.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index ffdc4f3ec6..57f1174d59 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -120,7 +120,7 @@ G. Dowek, allowed hierarchical developments of mathematical theories. This high-level language was called the *Mathematical Vernacular*. Furthermore, an interactive *Theorem Prover* permitted the incremental construction of proof trees in a top-down manner, subgoaling recursively -and backtracking from dead-alleys. The theorem prover executed tactics +and backtracking from dead-ends. The theorem prover executed tactics written in CAML, in the LCF fashion. A basic set of tactics was predefined, which the user could extend by his own specific tactics. This system (Version 4.10) was released in 1989. Then, the system was |