diff -r 0d689d71dbdc -r 5c32a072ca8b src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Oct 09 19:10:52 2017 +0200
+++ b/src/Doc/System/Sessions.thy	Wed Oct 11 20:16:00 2017 +0200
@@ -280,6 +280,7 @@
     -b           build heap images
     -c           clean build
     -d DIR       include session directory
+    -f           fresh build
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -k KEYWORD   check theory sources for conflicts with proposed keywords
@@ -365,6 +366,10 @@
   performing the specified build operation.
 
   \<^medskip>
+  Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
+  requirements.
+
+  \<^medskip>
   Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage
   (including optional cleanup). Note that the return code always indicates the
   status of the set of selected sessions.