more convenient export;
authorwenzelm
Tue, 02 Apr 2019 13:22:16 +0200
changeset 70208 6ae9505d693a
parent 70207 16042475c511
child 70211 b5574e88092b
child 70213 2dfba895e26d
more convenient export;
NEWS
src/HOL/ROOT
--- 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
--- 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]