diff options
| author | Sam Pablo Kuper | 2018-10-19 04:45:33 +0100 |
|---|---|---|
| committer | Sam Pablo Kuper | 2018-10-19 04:45:33 +0100 |
| commit | 5fb1677a4bf62155ef0f57c0a0b189d42e05505f (patch) | |
| tree | bed5fb47fa230c70cb1173d421ab906217a3109c /doc | |
| parent | c3823156da73a63967d9d472e21560af1585b271 (diff) | |
Replace non-idiomatic "dead-alleys" with idiomatic "dead-ends"
Diffstat (limited to 'doc')
| -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 |