1.1 --- a/src/HOL/ROOT	Wed Jul 25 10:55:02 2012 +0200
     1.2 +++ b/src/HOL/ROOT	Wed Jul 25 11:59:22 2012 +0200
     1.3 @@ -290,7 +290,7 @@
     1.4    files "document/root.bib" "document/root.tex"
     1.5  
     1.6  session Decision_Procs = HOL +
     1.7 -  options [document = false]
     1.8 +  options [condition = ISABELLE_POLYML, document = false]
     1.9    theories Decision_Procs
    1.10  
    1.11  session ex in "Proofs/ex" = "HOL-Proofs" +
    1.12 @@ -299,7 +299,7 @@
    1.13  
    1.14  session Extraction in "Proofs/Extraction" = "HOL-Proofs" +
    1.15    description {* Examples for program extraction in Higher-Order Logic *}
    1.16 -  options [proofs = 2, parallel_proofs = 0]
    1.17 +  options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
    1.18    theories [document = false]
    1.19      "~~/src/HOL/Library/Efficient_Nat"
    1.20      "~~/src/HOL/Library/Monad_Syntax"
    1.21 @@ -395,6 +395,7 @@
    1.22  
    1.23  session ex = HOL +
    1.24    description {* Miscellaneous examples for Higher-Order Logic. *}
    1.25 +  options [condition = ISABELLE_POLYML]
    1.26    theories [document = false]
    1.27      "~~/src/HOL/Library/State_Monad"
    1.28      Code_Nat_examples
    1.29 @@ -559,7 +560,7 @@
    1.30      "document/root.tex"
    1.31  
    1.32  session "HOL-Probability"! in "Probability" = "HOL-Multivariate_Analysis" +
    1.33 -  options [document_graph]
    1.34 +  options [condition = ISABELLE_POLYML, document_graph]
    1.35    theories [document = false]
    1.36      "~~/src/HOL/Library/Countable"
    1.37      "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
    1.38 @@ -575,7 +576,7 @@
    1.39    theories Nominal
    1.40  
    1.41  session Examples in "Nominal/Examples" = "HOL-Nominal" +
    1.42 -  options [document = false]
    1.43 +  options [condition = ISABELLE_POLYML, document = false]
    1.44    theories Nominal_Examples
    1.45    theories [quick_and_dirty] VC_Condition
    1.46