more convenient export;
authorwenzelm
Tue Apr 02 13:22:16 2019 +0200 (5 months ago)
changeset 700266ae9505d693a
parent 70025 16042475c511
child 70029 b5574e88092b
child 70031 2dfba895e26d
more convenient export;
NEWS
src/HOL/ROOT
     1.1 --- a/NEWS	Tue Apr 02 13:15:52 2019 +0200
     1.2 +++ b/NEWS	Tue Apr 02 13:22:16 2019 +0200
     1.3 @@ -212,9 +212,8 @@
     1.4  
     1.5  * Session HOL-SPARK: .prv files are no longer written to the
     1.6  file-system, but exported to the session database. Results may be
     1.7 -retrieved with the "isabelle export" command-line tool like this:
     1.8 -
     1.9 -  isabelle export -x "*:**.prv" HOL-SPARK-Examples
    1.10 +retrieved via "isabelle build -e HOL-SPARK-Examples" on the
    1.11 +command-line.
    1.12  
    1.13  * Sledgehammer:
    1.14    - The URL for SystemOnTPTP, which is used by remote provers, has been
     2.1 --- a/src/HOL/ROOT	Tue Apr 02 13:15:52 2019 +0200
     2.2 +++ b/src/HOL/ROOT	Tue Apr 02 13:22:16 2019 +0200
     2.3 @@ -874,6 +874,7 @@
     2.4      "RIPEMD-160/S_L"
     2.5      "RIPEMD-160/S_R"
     2.6      "Sqrt/Sqrt"
     2.7 +  export_files (in ".") "*:**.prv"
     2.8  
     2.9  session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
    2.10    options [show_question_marks = false]