no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";
authorwenzelm
Fri Nov 14 21:36:50 2014 +0100 (2014-11-14)
changeset 59006272d7fb92396
parent 59005 1c54ebc68394
child 59007 059ba950a657
no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";
src/HOL/ROOT
     1.1 --- a/src/HOL/ROOT	Fri Nov 14 17:07:06 2014 +0100
     1.2 +++ b/src/HOL/ROOT	Fri Nov 14 21:36:50 2014 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4    description {*
     1.5      HOL-Main with explicit proof terms.
     1.6    *}
     1.7 -  options [document = false]
     1.8 +  options [document = false, quick_and_dirty = false]
     1.9    theories Proofs (*sequential change of global flag!*)
    1.10    theories "~~/src/HOL/Library/Old_Datatype"
    1.11    files
    1.12 @@ -400,7 +400,7 @@
    1.13    description {*
    1.14      Examples for program extraction in Higher-Order Logic.
    1.15    *}
    1.16 -  options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0]
    1.17 +  options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0, quick_and_dirty = false]
    1.18    theories [document = false]
    1.19      "~~/src/HOL/Library/Code_Target_Numeral"
    1.20      "~~/src/HOL/Library/Monad_Syntax"
    1.21 @@ -425,7 +425,8 @@
    1.22      The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
    1.23      theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
    1.24    *}
    1.25 -  options [document_graph, print_mode = "no_brackets", parallel_proofs = 0]
    1.26 +  options [document_graph, print_mode = "no_brackets", parallel_proofs = 0,
    1.27 +    quick_and_dirty = false]
    1.28    theories [document = false]
    1.29      "~~/src/HOL/Library/Code_Target_Int"
    1.30    theories