From f4f8faf0c151ad81009b5f21c9fe8becf7fa7bba Mon Sep 17 00:00:00 2001 From: Pierre Casteran Date: Thu, 19 May 2022 15:32:44 +0200 Subject: [PATCH] small changes description --- v09changes.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/v09changes.md b/v09changes.md index 3951554d..89dee530 100644 --- a/v09changes.md +++ b/v09changes.md @@ -1,4 +1,4 @@ -The experimental bridge to the [Gaia project](https://github.com/coq-community/gaia) allows now to import some definitions and theorems of the Ketonen-Solovay combinatorial theorems into the Gaia environment (see Chapter 7 of [the documentation](https://coq-community.org/hydra-battles/doc/hydras.pdf)). +The experimental bridge to the [Gaia project](https://github.com/coq-community/gaia) allows now to import some definitions and theorems of the so-called Ketonen-Solovay combinatorial machinery into the Gaia environment (see Chapter 7 of [the documentation](https://coq-community.org/hydra-battles/doc/hydras.pdf)). The first topics treated in this version are: canonical sequences, accessibility, and a few rapidly growing hierarchies of arithmetical functions.