--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/Nominal_Examples.thy Mon Sep 21 16:01:30 2009 +0200
@@ -0,0 +1,25 @@
+(* Author: Christian Urban TU Muenchen *)
+
+header {* Various examples involving nominal datatypes. *}
+
+theory Nominal_Examples
+imports
+ CR
+ CR_Takahashi
+ Class
+ Compile
+ Fsub
+ Height
+ Lambda_mu
+ SN
+ Weakening
+ Crary
+ SOS
+ LocalWeakening
+ Support
+ Contexts
+ Standardization
+ W
+begin
+
+end
--- a/src/HOL/Nominal/Examples/ROOT.ML Mon Sep 21 16:00:53 2009 +0200
+++ b/src/HOL/Nominal/Examples/ROOT.ML Mon Sep 21 16:01:30 2009 +0200
@@ -1,27 +1,4 @@
-(* Title: HOL/Nominal/Examples/ROOT.ML
- ID: $Id$
- Author: Christian Urban, TU Muenchen
-
-Various examples involving nominal datatypes.
-*)
-use_thys [
- "CR",
- "CR_Takahashi",
- "Class",
- "Compile",
- "Fsub",
- "Height",
- "Lambda_mu",
- "SN",
- "Weakening",
- "Crary",
- "SOS",
- "LocalWeakening",
- "Support",
- "Contexts",
- "Standardization",
- "W"
-];
+use_thy "Nominal_Examples";
-setmp_noncritical quick_and_dirty true use_thy "VC_Condition";
+setmp_noncritical quick_and_dirty true use_thy "VC_Condition"; (*FIXME*)