clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
(* :mode=isabelle-options: *)
section "HOL-SPARK"
option spark_prv : bool = true
-- "produce proof review file after 'spark_end'"