diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index ca6882c..3c20191 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -14,14 +14,15 @@
     - [SANY]()
     - [Java Path Finder](./codebase/jpf.md)
     - []()
-- [Learning TLA+](./learning/intro.md)
+- [Learning TLA+: Introduction](./learning/intro.md)
     - [Lamport's video tutorial]()
+    - [Hyperbook]()
     - [Example repo]()
     - [Notable repos]()
     - [Books]()
     - [TLA]()
         - [Typed Model Values]()
-    - [Pluscal]()
+    - [Pluscal](./learning/pluscal.md)
         - []()
     - [TLA+ Vs xxx](./learning/tla-comparisons.md)
     - [Config files](./learning/config-file.md)
diff --git a/src/codebase/jpf.md b/src/codebase/jpf.md
index 25745c0..d3d2465 100644
--- a/src/codebase/jpf.md
+++ b/src/codebase/jpf.md
@@ -1,5 +1,9 @@
 # Java Path Finder
-Java Path Finder is a project developed by nasa for model checking Java bytecode. See [https://github.com/javapathfinder/jpf-core](https://github.com/javapathfinder/jpf-core).
+Java Path Finder is a project developed by Nasa for model checking Java bytecode. See [https://github.com/javapathfinder/jpf-core](https://github.com/javapathfinder/jpf-core).
 
-JPF is used to test some of the tla+ classes.
+JPF is used to test some of the datastructures of tlatools. These tests can be invoked by using:
+
+```
+ant -f customBuild.xml compile compile-test test-verify
+```