--- 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
--- 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]