--- a/src/HOL/ROOT Sat Feb 13 11:50:01 2016 +0100
+++ b/src/HOL/ROOT Sat Feb 13 12:13:10 2016 +0100
@@ -788,7 +788,7 @@
session "HOL-Datatype_Examples" in Datatype_Examples = HOL +
description {*
- (Co)datatype Examples, including large ones from John Harrison.
+ (Co)datatype Examples.
*}
options [document = false]
theories
@@ -807,10 +807,6 @@
Misc_Datatype
Misc_Primcorec
Misc_Primrec
- theories [condition = ISABELLE_FULL_TEST]
- Brackin
- IsaFoR
- Misc_N2M
session "HOL-Word" (main) in Word = HOL +
theories Word
@@ -964,13 +960,6 @@
Hotel_Example
Quickcheck_Narrowing_Examples
-session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
- theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
- Find_Unused_Assms_Examples
- Needham_Schroeder_No_Attacker_Example
- Needham_Schroeder_Guided_Attacker_Example
- Needham_Schroeder_Unguided_Attacker_Example
-
session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
description {*
Author: Cezary Kaliszyk and Christian Urban
@@ -1139,12 +1128,3 @@
theories
TrivEx
TrivEx2
-
-session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
- description {*
- Some benchmark on large record.
- *}
- options [document = false]
- theories [condition = ISABELLE_FULL_TEST]
- Record_Benchmark
-