src/HOL/ROOT

 
 session "HOL-Proofs" (slow) = Pure +
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [condition = ML_SYSTEM_POLYML, document = false, quick_and_dirty = false]
+  options [document = false, quick_and_dirty = false]
   theories Proofs (*sequential change of global flag!*)
   theories "~~/src/HOL/Library/Old_Datatype"
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"

   *}
   theories Hoare_Parallel
   document_files "root.bib" "root.tex"
 
 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
-  options [condition = ML_SYSTEM_POLYML, document = false, browser_info = false]
+  options [document = false, browser_info = false]
   theories
     Generate
     Generate_Binary_Nat
     Generate_Target_Nat
     Generate_Efficient_Datastructures
     Generate_Pretty_Char
-  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_GHC"]
+  theories [condition = "ISABELLE_GHC"]
     Code_Test_GHC
-  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_MLTON"]
+  theories [condition = "ISABELLE_MLTON"]
     Code_Test_MLton
-  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_OCAMLC"]
+  theories [condition = "ISABELLE_OCAMLC"]
     Code_Test_OCaml
-  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_POLYML"]
+  theories [condition = "ISABELLE_POLYML"]
     Code_Test_PolyML
-  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_SCALA"]
+  theories [condition = "ISABELLE_SCALA"]
     Code_Test_Scala
-  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_SMLNJ"]
+  theories [condition = "ISABELLE_SMLNJ"]
     Code_Test_SMLNJ
 
 session "HOL-Metis_Examples" in Metis_Examples = HOL +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

 
 session "HOL-Decision_Procs" in Decision_Procs = HOL +
   description {*
     Various decision procedures, typically involving reflection.
   *}
-  options [condition = ML_SYSTEM_POLYML, document = false]
+  options [document = false]
   theories Decision_Procs
 
 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
-  options [condition = ML_SYSTEM_POLYML, document = false, parallel_proofs = 0]
+  options [document = false, parallel_proofs = 0]
   theories
     Hilbert_Classical
     XML_Data
 
 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
   description {*
     Examples for program extraction in Higher-Order Logic.
   *}
-  options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0, quick_and_dirty = false]
+  options [parallel_proofs = 0, quick_and_dirty = false]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Monad_Syntax"
     "~~/src/HOL/Number_Theory/Primes"
     "~~/src/HOL/Number_Theory/UniqueFactorization"

     proves confluence of beta, eta and beta+eta.
 
     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   *}
-  options [condition = ML_SYSTEM_POLYML, print_mode = "no_brackets",
+  options [print_mode = "no_brackets",
     parallel_proofs = 0, quick_and_dirty = false]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Int"
   theories
     Eta

 
 session "HOL-ex" in ex = HOL +
   description {*
     Miscellaneous examples for Higher-Order Logic.
   *}
-  options [condition = ML_SYSTEM_POLYML]
   theories [document = false]
     "~~/src/HOL/Library/State_Monad"
     Code_Binary_Nat_examples
     "~~/src/HOL/Library/FuncSet"
     Eval_Examples

     Author:     Nik Sultana, University of Cambridge
     Copyright   2011
 
     TPTP-related extensions.
   *}
-  options [condition = ML_SYSTEM_POLYML, document = false]
+  options [document = false]
   theories
     ATP_Theory_Export
     MaSh_Eval
     TPTP_Interpret
     THF_Arith

 session "HOL-Nominal" in Nominal = HOL +
   options [document = false]
   theories Nominal
 
 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
-  options [condition = ML_SYSTEM_POLYML, document = false]
+  options [document = false]
   theories
     Class3
     CK_Machine
     Compile
     Contexts

 session "HOL-Mirabelle" in Mirabelle = HOL +
   options [document = false]
   theories Mirabelle_Test
 
 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
-  options [condition = ML_SYSTEM_POLYML, document = false, timeout = 60]
+  options [document = false, timeout = 60]
   theories Ex
 
 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
-  options [condition = ML_SYSTEM_POLYML, document = false, quick_and_dirty]
+  options [document = false, quick_and_dirty]
   theories
     Boogie
     SMT_Examples
     SMT_Word_Examples
     SMT_Tests

     Int_Pow
     Lifting_Code_Dt_Test
 
 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   options [document = false]
-  theories [condition = ML_SYSTEM_POLYML]
+  theories
     Examples
     Predicate_Compile_Tests
     Predicate_Compile_Quickcheck_Examples
     Specialisation_Examples
     IMP_1