diff --git a/README.md b/README.md
index ebde2af0..62d31e7d 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,10 @@
 What4 is a library for representing symbolic terms and communicating with
 satisfiability and SMT solvers (e.g. Yices and Z3).
 
-It was originally a part of the Crucible (https://github.com/GaloisInc/crucible)
+It was originally a part of the [Crucible](https://github.com/GaloisInc/crucible)
 project, but has found use cases that are independent of its original
 purpose as the representation language for the Crucible symbolic
 simulator, and has thus been split out into a separate repository.
+
+For an overview of What4 and how to use it, check out the
+package-level [README](what4/README.md).