From 78f5c8ed483f8c52e902b0c6eb6beb359b5df19c Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 18 Sep 2018 11:45:22 +0200
Subject: Update README.md

---
 README.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/README.md b/README.md
index 2346a6a..d6860b1 100644
--- a/README.md
+++ b/README.md
@@ -2,6 +2,12 @@
 
 An experimental implementation of [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) in the interactive theorem prover [Isabelle](https://isabelle.in.tum.de/).
 
+### Usage
+
+The default entry point for the logic is `HoTT`, which loads everything else.
+
+You can also load theories selectively, in this case,`HoTT_Base` is required and `HoTT_Methods` is helpful.
+
 ### License
 
 GNU LGPLv3
-- 
cgit v1.2.3