# HG changeset patch
# User blanchet
# Date 1410457102 -7200
# Node ID 710f56e192fee163b468a617dff095a2e929b301
# Parent  a684dd412115ef521841543e988ed6c9379a34d7
updated ROOT

diff -r a684dd412115 -r 710f56e192fe src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Sep 11 19:35:38 2014 +0200
+++ b/src/HOL/ROOT	Thu Sep 11 19:38:22 2014 +0200
@@ -732,7 +732,7 @@
 
 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
@@ -748,7 +748,7 @@
     Misc_Datatype
     Misc_Primcorec
     Misc_Primrec
-  theories [condition = ISABELLE_FULL_TEST]
+  theories [condition = ISABELLE_FULL_TEST, timing]
     Brackin
     Instructions
     IsaFoR_Datatypes
@@ -1085,17 +1085,6 @@
     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.