src/HOL/ROOT

     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
 
     Testing Metis and Sledgehammer.
   *}
-  options [document = false]
+  options [timeout = 3600, document = false]
   theories
     Abstraction
     Big_O
     Binary_Tree
     Clausification

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

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

 session Mutabelle = HOL +
   options [document = false]
   theories MutabelleExtra
 
 session Quickcheck_Examples = HOL +
-  options [document = false]
+  options [timeout = 3600, document = false]
   theories
     Quickcheck_Examples (* FIXME more *)
   theories [condition = ISABELLE_GHC]
     Quickcheck_Narrowing_Examples