--- 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.