discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
authorwenzelm
Sun Jun 30 12:30:02 2013 +0200 (2013-06-30)
changeset 52488cd65ee49a8ba
parent 52487 48bc24467008
child 52489 a36ba4d2819a
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
discontinued unused proofterms for FOL;
NEWS
etc/options
src/Doc/ROOT
src/FOL/ROOT
src/HOL/Proofs.thy
src/HOL/ROOT
src/Pure/Tools/build.ML
     1.1 --- a/NEWS	Sun Jun 30 11:37:34 2013 +0200
     1.2 +++ b/NEWS	Sun Jun 30 12:30:02 2013 +0200
     1.3 @@ -50,6 +50,11 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* System option "proofs" has been discontinued.  Instead the global
     1.8 +state of Proofterm.proofs is persistently compiled into logic images
     1.9 +as required, notably HOL-Proofs.  Users no longer need to change
    1.10 +Proofterm.proofs dynamically.  Minor INCOMPATIBILITY.
    1.11 +
    1.12  * Syntax translation functions (print_translation etc.) always depend
    1.13  on Proof.context.  Discontinued former "(advanced)" option -- this is
    1.14  now the default.  Minor INCOMPATIBILITY.
     2.1 --- a/etc/options	Sun Jun 30 11:37:34 2013 +0200
     2.2 +++ b/etc/options	Sun Jun 30 12:30:02 2013 +0200
     2.3 @@ -79,8 +79,6 @@
     2.4  
     2.5  section "Detail of Proof Recording"
     2.6  
     2.7 -option proofs : int = 1
     2.8 -  -- "level of detail for proof objects: 0, 1, 2"
     2.9  option quick_and_dirty : bool = false
    2.10    -- "if true then some tools will OMIT some proofs"
    2.11  option skip_proofs : bool = false
     3.1 --- a/src/Doc/ROOT	Sun Jun 30 11:37:34 2013 +0200
     3.2 +++ b/src/Doc/ROOT	Sun Jun 30 12:30:02 2013 +0200
     3.3 @@ -81,7 +81,7 @@
     3.4      Proof
     3.5      Syntax
     3.6      Tactic
     3.7 -  theories [proofs = 2, skip_proofs = false, parallel_proofs = 0]
     3.8 +  theories [skip_proofs = false, parallel_proofs = 0]
     3.9      Logic
    3.10    files
    3.11      "../prepare_document"
     4.1 --- a/src/FOL/ROOT	Sun Jun 30 11:37:34 2013 +0200
     4.2 +++ b/src/FOL/ROOT	Sun Jun 30 12:30:02 2013 +0200
     4.3 @@ -15,7 +15,6 @@
     4.4  
     4.5      Michael Dummett, Elements of Intuitionism (Oxford, 1977)
     4.6    *}
     4.7 -  options [proofs = 2]
     4.8    theories FOL
     4.9    files "document/root.tex"
    4.10  
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Proofs.thy	Sun Jun 30 12:30:02 2013 +0200
     5.3 @@ -0,0 +1,8 @@
     5.4 +theory Proofs
     5.5 +imports Pure
     5.6 +begin
     5.7 +
     5.8 +ML "Proofterm.proofs := 2"
     5.9 +
    5.10 +end
    5.11 +
     6.1 --- a/src/HOL/ROOT	Sun Jun 30 11:37:34 2013 +0200
     6.2 +++ b/src/HOL/ROOT	Sun Jun 30 12:30:02 2013 +0200
     6.3 @@ -16,7 +16,8 @@
     6.4    description {*
     6.5      HOL-Main with explicit proof terms.
     6.6    *}
     6.7 -  options [document = false, proofs = 2, skip_proofs = false]
     6.8 +  options [document = false, skip_proofs = false]
     6.9 +  theories Proofs (*sequential change of global flag!*)
    6.10    theories Main
    6.11    files
    6.12      "Tools/Quickcheck/Narrowing_Engine.hs"
    6.13 @@ -356,7 +357,7 @@
    6.14    theories Decision_Procs
    6.15  
    6.16  session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
    6.17 -  options [document = false, proofs = 2, skip_proofs = false, parallel_proofs = 0]
    6.18 +  options [document = false, skip_proofs = false, parallel_proofs = 0]
    6.19    theories
    6.20      Hilbert_Classical
    6.21      XML_Data
    6.22 @@ -365,7 +366,7 @@
    6.23    description {*
    6.24      Examples for program extraction in Higher-Order Logic.
    6.25    *}
    6.26 -  options [condition = ISABELLE_POLYML, proofs = 2, skip_proofs = false, parallel_proofs = 0]
    6.27 +  options [condition = ISABELLE_POLYML, skip_proofs = false, parallel_proofs = 0]
    6.28    theories [document = false]
    6.29      "~~/src/HOL/Library/Code_Target_Numeral"
    6.30      "~~/src/HOL/Library/Monad_Syntax"
    6.31 @@ -390,8 +391,7 @@
    6.32      The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
    6.33      theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
    6.34    *}
    6.35 -  options [document_graph, print_mode = "no_brackets", proofs = 2, skip_proofs = false,
    6.36 -    parallel_proofs = 0]
    6.37 +  options [document_graph, print_mode = "no_brackets", skip_proofs = false, parallel_proofs = 0]
    6.38    theories [document = false]
    6.39      "~~/src/HOL/Library/Code_Target_Int"
    6.40    theories
    6.41 @@ -652,7 +652,7 @@
    6.42      MaSh_Export
    6.43      TPTP_Interpret
    6.44      THF_Arith
    6.45 -  theories [proofs = 0]  (* FIXME !? *)
    6.46 +  theories
    6.47      ATP_Problem_Import
    6.48  
    6.49  session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
     7.1 --- a/src/Pure/Tools/build.ML	Sun Jun 30 11:37:34 2013 +0200
     7.2 +++ b/src/Pure/Tools/build.ML	Sun Jun 30 12:30:02 2013 +0200
     7.3 @@ -102,7 +102,6 @@
     7.4  
     7.5  fun use_theories last_timing options =
     7.6    Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
     7.7 -    |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
     7.8      |> Unsynchronized.setmp print_mode
     7.9          (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    7.10      |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")