diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt
index 3c741cf1..67a5436e 100644
--- a/prism/CHANGELOG.txt
+++ b/prism/CHANGELOG.txt
@@ -2,27 +2,32 @@ This file contains details of the changes in each new version of PRISM.
 
 New since last release:
 
-* Fixed building on new versions of Cygwin (Windows)
-* Export steady-state/transient probabilities from GUI
-* Additional graph zoom functionality on popup menu
-* Added R[C<=k] operator for MDPs (sparse, explicit)
-* Additional functionality in explicit engine
-  - export BSCCs, some LTL
-* New -exportmecs and -exportsccs switches
-* New -sumroundoff switch (used when checking probabilities sum to 1)
-* Update CUDD to version 2.5.0
-* Strategy generation:
-  - improvements in explicit engine implementation
-  - new -exportstrat switch, in development
-* Integer variables can be unbounded (e.g. "x:int;"), for simulation only
-* Small improvements to usability of the GUI simulator transition table
-* Slight change to notation for -exportresults to match -exportmodel
-* Some new '-help xxx' switches (const,simpath,exportresults,aroptions,exportmodel,importmodel)
-* New -exportmodel and -importmodel convenience switches
-* Allow command-line switches of form --sw (as well as -sw)
 * Parametric model checking
-* Fast adaptive uniformisation
-* Export/view labels from GUI
+
+* New model checking and export functionality
+  - fast adaptive uniformisation for CTMC transient analysis
+  - added R[C<=k] operator for MDPs (sparse, explicit)
+  - new -exportmecs and -exportsccs switches
+  - additional functionality in explicit engine (export BSCCs, LTL)
+  - improved adversary.strategy generation in explicit engine
+  - integer variables can be unbounded (e.g. "x:int;"), for simulation-based analysis
+
+* New options/switches:
+  - new -exportmodel and -importmodel convenience switches
+  - new -sumroundoff switch (used when checking probabilities sum to 1)
+  - some new '-help xxx' switches (const,simpath,exportresults,aroptions,exportmodel,importmodel)
+  - allow command-line switches of form --sw (as well as -sw)
+  - slight change to notation for -exportresults to match -exportmodel
+
+* Additional functionality available in GUI:
+  - export steady-state/transient probabilities from GUI
+  - export/view labels from model/properties from GUI
+  - small improvements to usability of the GUI simulator transition table
+  - additional graph zoom functionality on popup menu
+
+* Updates to build process
+  - fixed building on new versions of Cygwin (Windows)
+  - update CUDD to version 2.5.0
 
 -----------------------------------------------------------------------------
 Version 4.1 (first released 20/12/2012)