diff --git a/README.md b/README.md
index dd374cd8..f8aaf63a 100644
--- a/README.md
+++ b/README.md
@@ -33,20 +33,19 @@ This might cause Isabelle/jEdit to pause PSL's proof search after reaching its d
 ![Screenshot](./image/tracing_messages.png)
 
 ## Contents
-- `.src/Utils.ML` includes various utility functions.
-- `.src/Subtool.ML` treats Isabelle's subtools as state-monad tactics.
-- `.src/Dynamic_Tactic_Generation.ML` facilitates runtime tactic generation.
-- `.src/Constructor_Class.ML/` is a general purpose constructor class library.
-- `.src/Instantiation.ML` instantiates some type constructors as members of constructor classes.
-- `.src/Monadic_Prover.ML` contains the interpreter of PSL.
-- `.src/Parser_Combinator.ML` contains general purpose monadic parser combinators.
-- `.src/PSL_Parser.ML` defines the PSL parser.
-- `.src/Isar_Interface.thy` sets up the Isabelle/Isar interface for PSL.
-- `.src/Try_Hard.thy` defines the default strategy try_hard.
-- `./PSL.thy` reads all the necessary files to use PSL and try_hard.
-- `./Example` presents small example strategies and use cases.
+- `PSL/Utils.ML` includes various utility functions.
+- `PSL/Subtool.ML` treats Isabelle's subtools as state-monad tactics.
+- `PSL/Dynamic_Tactic_Generation.ML` facilitates runtime tactic generation.
+- `PSL/Constructor_Class.ML/` is a general purpose constructor class library.
+- `PSL/Instantiation.ML` instantiates some type constructors as members of constructor classes.
+- `PSL/Monadic_Prover.ML` contains the interpreter of PSL.
+- `PSL/Parser_Combinator.ML` contains general purpose monadic parser combinators.
+- `PSL/PSL_Parser.ML` defines the PSL parser.
+- `PSL/Isar_Interface.thy` sets up the Isabelle/Isar interface for PSL.
+- `PSL/Try_Hard.thy` defines the default strategy try_hard.
+- `PSL/PSL.thy` reads all the necessary files to use PSL and try_hard.
+- `Example/Example.thy` presents small example strategies and use cases.
 - `PaMpeR/` is a tool for **p**roof **m**thod **r**commendation.
-- `PGT/` is our conjecturing mechanism, **p**roof **g**oal **t**ransformer.
 - `MeLoId/` is work in progress.
 - `LiFtEr/` is a language to encode induction heuristics.