src/HOL/ROOT
changeset 58413 22dd971f6938
parent 58385 9cbef70cff8e
child 58415 8392d221bd91
     1.1 --- a/src/HOL/ROOT	Sun Sep 21 20:14:04 2014 +0200
     1.2 +++ b/src/HOL/ROOT	Sun Sep 21 20:22:12 2014 +0200
     1.3 @@ -388,7 +388,7 @@
     1.4    description {*
     1.5      Various decision procedures, typically involving reflection.
     1.6    *}
     1.7 -  options [condition = ISABELLE_POLYML, document = false]
     1.8 +  options [condition = ML_SYSTEM_POLYML, document = false]
     1.9    theories Decision_Procs
    1.10  
    1.11  session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
    1.12 @@ -401,7 +401,7 @@
    1.13    description {*
    1.14      Examples for program extraction in Higher-Order Logic.
    1.15    *}
    1.16 -  options [condition = ISABELLE_POLYML, parallel_proofs = 0]
    1.17 +  options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0]
    1.18    theories [document = false]
    1.19      "~~/src/HOL/Library/Code_Target_Numeral"
    1.20      "~~/src/HOL/Library/Monad_Syntax"
    1.21 @@ -524,7 +524,7 @@
    1.22    description {*
    1.23      Miscellaneous examples for Higher-Order Logic.
    1.24    *}
    1.25 -  options [timeout = 3600, condition = ISABELLE_POLYML]
    1.26 +  options [timeout = 3600, condition = ML_SYSTEM_POLYML]
    1.27    theories [document = false]
    1.28      "~~/src/HOL/Library/State_Monad"
    1.29      Code_Binary_Nat_examples
    1.30 @@ -719,7 +719,7 @@
    1.31    theories Nominal
    1.32  
    1.33  session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
    1.34 -  options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
    1.35 +  options [timeout = 3600, condition = ML_SYSTEM_POLYML, document = false]
    1.36    theories
    1.37      Nominal_Examples_Base
    1.38    theories [condition = ISABELLE_FULL_TEST]