# HG changeset patch
# User wenzelm
# Date 1554204136 -7200
# Node ID 6ae9505d693a459e35be86141ffa0b69b0d0ef06
# Parent  16042475c511256696273e887813c1c0dc3e938c
more convenient export;

diff -r 16042475c511 -r 6ae9505d693a NEWS
--- a/NEWS	Tue Apr 02 13:15:52 2019 +0200
+++ b/NEWS	Tue Apr 02 13:22:16 2019 +0200
@@ -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 16042475c511 -r 6ae9505d693a src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Apr 02 13:15:52 2019 +0200
+++ b/src/HOL/ROOT	Tue Apr 02 13:22:16 2019 +0200
@@ -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]