# HG changeset patch
# User wenzelm
# Date 1419030320 -3600
# Node ID dca5594761f2a6c937891da8ad7cf87b7daab3e1
# Parent  5a13df748faced556905ab2e1b7c84a77f0e2694
afford full test, with slightly improved scheduling order;

diff -r 5a13df748fac -r dca5594761f2 src/HOL/Nominal/Examples/Nominal_Examples.thy
--- a/src/HOL/Nominal/Examples/Nominal_Examples.thy	Fri Dec 19 23:33:08 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(*  Author:  Christian Urban TU Muenchen *)
-
-section {* Various examples involving nominal datatypes. *}
-
-theory Nominal_Examples
-imports Nominal_Examples_Base Class3
-begin
-
-end
diff -r 5a13df748fac -r dca5594761f2 src/HOL/Nominal/Examples/Nominal_Examples_Base.thy
--- a/src/HOL/Nominal/Examples/Nominal_Examples_Base.thy	Fri Dec 19 23:33:08 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Author:  Christian Urban TU Muenchen *)
-
-section {* 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 5a13df748fac -r dca5594761f2 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Dec 19 23:33:08 2014 +0100
+++ b/src/HOL/ROOT	Sat Dec 20 00:05:20 2014 +0100
@@ -725,9 +725,26 @@
 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   options [condition = ML_SYSTEM_POLYML, document = false]
   theories
-    Nominal_Examples_Base
-  theories [condition = ISABELLE_FULL_TEST]
-    Nominal_Examples
+    Class3
+    CK_Machine
+    Compile
+    Contexts
+    Crary
+    CR_Takahashi
+    CR
+    Fsub
+    Height
+    Lambda_mu
+    Lam_Funs
+    LocalWeakening
+    Pattern
+    SN
+    SOS
+    Standardization
+    Support
+    Type_Preservation
+    Weakening
+    W
   theories [quick_and_dirty]
     VC_Condition