src/HOL/ROOT

     "~~/src/HOL/Library/LaTeXsugar"
   theories Imperative_HOL_ex
   files "document/root.bib" "document/root.tex"
 
 session Decision_Procs = HOL +
-  options [document = false]
+  options [condition = ISABELLE_POLYML, document = false]
   theories Decision_Procs
 
 session ex in "Proofs/ex" = "HOL-Proofs" +
   options [document = false, proofs = 2, parallel_proofs = 0]
   theories Hilbert_Classical
 
 session Extraction in "Proofs/Extraction" = "HOL-Proofs" +
   description {* Examples for program extraction in Higher-Order Logic *}
-  options [proofs = 2, parallel_proofs = 0]
+  options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
   theories [document = false]
     "~~/src/HOL/Library/Efficient_Nat"
     "~~/src/HOL/Library/Monad_Syntax"
     "~~/src/HOL/Number_Theory/Primes"
     "~~/src/HOL/Number_Theory/UniqueFactorization"

   theories CompleteLattice
   files "document/root.tex"
 
 session ex = HOL +
   description {* Miscellaneous examples for Higher-Order Logic. *}
+  options [condition = ISABELLE_POLYML]
   theories [document = false]
     "~~/src/HOL/Library/State_Monad"
     Code_Nat_examples
     "~~/src/HOL/Library/FuncSet"
     Eval_Examples

   files
     "Integration.certs"
     "document/root.tex"
 
 session "HOL-Probability"! in "Probability" = "HOL-Multivariate_Analysis" +
-  options [document_graph]
+  options [condition = ISABELLE_POLYML, document_graph]
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
     "~~/src/HOL/Library/Permutation"
   theories

 session Nominal (2) = HOL +
   options [document = false]
   theories Nominal
 
 session Examples in "Nominal/Examples" = "HOL-Nominal" +
-  options [document = false]
+  options [condition = ISABELLE_POLYML, document = false]
   theories Nominal_Examples
   theories [quick_and_dirty] VC_Condition
 
 session Word = HOL +
   options [document_graph]