Update README.md

Author: wenkokke

README.md

@@ -65,10 +65,7 @@ agda-mode setup
 
 To load and type-check the file, use [`C-c C-l`][agda-docs-emacs-notation].
 
-
-Agda is edited “interactively, which means that one can type check code which is not yet complete: if a question mark (?) is used as a placeholder for an expression, and the buffer is then checked, Agda will replace the question mark with a “hole” which can be filled in later. One can also do various other things in the context of a hole: listing the context, inferring the type of an expression, and even evaluating an open term which mentions variables bound in the surrounding context.”
-
-Agda is edited interactively, using “holes”, which are bits of the program that are not yet filled in. If you use a question mark as an expression, and load the buffer using `C-c C-l`, Agda replaces the question mark with a hole. There are several things you can to while the cursor is in a hole:
+Agda is edited interactively, using [“holes”][agda-docs-holes], which are bits of the program that are not yet filled in. If you use a question mark as an expression, and load the buffer using `C-c C-l`, Agda replaces the question mark with a hole. There are several things you can to while the cursor is in a hole:
 
     C-c C-c x    split on variable x
     C-c C-space  fill in hole
@@ -233,6 +230,7 @@ The EPUB is written to `out/epub/plfa.epub`.
 
 [agda]: https://github.com/agda/agda/releases/tag/v2.6.1
 [agda-version]: https://img.shields.io/badge/agda-v2.6.1-blue.svg
+[agda-docs-holes]: https://agda.readthedocs.io/en/v2.5.4/getting-started/quick-guide.html
 [agda-docs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html
 [agda-docs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html#notation-for-key-combinations
 [agda-docs-package-system]: https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html#example-using-the-standard-library