--- a/src/HOL/Nominal/Examples/Nominal_Examples.thy Fri Sep 12 13:50:55 2014 +0200
+++ b/src/HOL/Nominal/Examples/Nominal_Examples.thy Fri Sep 12 16:42:36 2014 +0200
@@ -3,26 +3,7 @@
header {* Various examples involving nominal datatypes. *}
theory Nominal_Examples
-imports
- CK_Machine
- CR
- CR_Takahashi
- Class3
- Compile
- Contexts
- Crary
- Fsub
- Height
- Lambda_mu
- LocalWeakening
- Pattern
- SN
- SOS
- Standardization
- Support
- Type_Preservation
- W
- Weakening
+imports Nominal_Examples_Base Class3
begin
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/Nominal_Examples_Base.thy Fri Sep 12 16:42:36 2014 +0200
@@ -0,0 +1,27 @@
+(* Author: Christian Urban TU Muenchen *)
+
+header {* Various examples involving nominal datatypes. *}
+
+theory Nominal_Examples_Base
+imports
+ CK_Machine
+ CR
+ CR_Takahashi
+ Compile
+ Contexts
+ Crary
+ Fsub
+ Height
+ Lambda_mu
+ LocalWeakening
+ Pattern
+ SN
+ SOS
+ Standardization
+ Support
+ Type_Preservation
+ W
+ Weakening
+begin
+
+end
--- a/src/HOL/ROOT Fri Sep 12 13:50:55 2014 +0200
+++ b/src/HOL/ROOT Fri Sep 12 16:42:36 2014 +0200
@@ -716,8 +716,12 @@
session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
- theories Nominal_Examples
- theories [quick_and_dirty] VC_Condition
+ theories
+ Nominal_Examples_Base
+ theories [condition = ISABELLE_FULL_TEST]
+ Nominal_Examples
+ theories [quick_and_dirty]
+ VC_Condition
session "HOL-Cardinals" in Cardinals = HOL +
description {*