# HG changeset patch
# User paulson
# Date 1554210112 -3600
# Node ID b5574e88092be5c213cf6154663f69fb61fa8e72
# Parent  6ae9505d693a459e35be86141ffa0b69b0d0ef06# Parent  e8da1fe4d61c45b5a73748e6f9de5ba666a8bd49
merged

diff -r e8da1fe4d61c -r b5574e88092b NEWS
--- a/NEWS	Tue Apr 02 12:56:21 2019 +0100
+++ b/NEWS	Tue Apr 02 14:01:52 2019 +0100
@@ -212,9 +212,8 @@
 
 * Session HOL-SPARK: .prv files are no longer written to the
 file-system, but exported to the session database. Results may be
-retrieved with the "isabelle export" command-line tool like this:
-
-  isabelle export -x "*:**.prv" HOL-SPARK-Examples
+retrieved via "isabelle build -e HOL-SPARK-Examples" on the
+command-line.
 
 * Sledgehammer:
   - The URL for SystemOnTPTP, which is used by remote provers, has been
diff -r e8da1fe4d61c -r b5574e88092b src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Apr 02 12:56:21 2019 +0100
+++ b/src/HOL/ROOT	Tue Apr 02 14:01:52 2019 +0100
@@ -874,6 +874,7 @@
     "RIPEMD-160/S_L"
     "RIPEMD-160/S_R"
     "Sqrt/Sqrt"
+  export_files (in ".") "*:**.prv"
 
 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   options [show_question_marks = false]