src/HOL/ROOT

     "root.tex"
     "root.bib"
 
 session "HOL-Datatype_Examples" in Datatype_Examples = HOL +
   description {*
-    (Co)datatype Examples.
+    (Co)datatype Examples, including large ones from John Harrison.
   *}
   options [document = false]
   theories
     Compat
     Lambda_Term

     Stream_Processor
     Misc_Codatatype
     Misc_Datatype
     Misc_Primcorec
     Misc_Primrec
-  theories [condition = ISABELLE_FULL_TEST]
+  theories [condition = ISABELLE_FULL_TEST, timing]
     Brackin
     Instructions
     IsaFoR_Datatypes
     SML
     Verilog

   options [document = false]
   theories
     TrivEx
     TrivEx2
 
-session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
-  description {*
-    Some rather large datatype examples (from John Harrison).
-  *}
-  options [document = false]
-  theories [condition = ISABELLE_FULL_TEST, timing]
-    Brackin
-    Instructions
-    SML
-    Verilog
-
 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
   description {*
     Some benchmark on large record.
   *}
   options [document = false]