# HG changeset patch
# User blanchet
# Date 1410532956 -7200
# Node ID a31404ec741473c6124824eac5fb3a8e84abdb71
# Parent  086193f231ea369895d810416005e47856a2cd42
run larger nominal examples only 'ISABELLE_FULL_TEST'

diff -r 086193f231ea -r a31404ec7414 src/HOL/Nominal/Examples/Nominal_Examples.thy
--- 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
diff -r 086193f231ea -r a31404ec7414 src/HOL/Nominal/Examples/Nominal_Examples_Base.thy
--- /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
diff -r 086193f231ea -r a31404ec7414 src/HOL/ROOT
--- 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 {*