diff -r 92dc6cfa3a95 -r 3772bb3bd7ce Nominal/Perm.thy
--- a/Nominal/Perm.thy	Wed Aug 25 22:55:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-theory Perm
-imports 
-  "../Nominal-General/Nominal2_Base"
-  "../Nominal-General/Nominal2_Atoms" 
-  "../Nominal-General/Nominal2_Eqvt" 
-  "Nominal2_FSet"
-  "Abs"
-uses ("nominal_dt_rawperm.ML")
-     ("nominal_dt_rawfuns.ML")
-     ("nominal_dt_alpha.ML")
-     ("nominal_dt_quot.ML")
-begin
-
-use "nominal_dt_rawperm.ML"
-ML {* open Nominal_Dt_RawPerm *}
-
-use "nominal_dt_rawfuns.ML"
-ML {* open Nominal_Dt_RawFuns *}
-
-use "nominal_dt_alpha.ML"
-ML {* open Nominal_Dt_Alpha *}
-
-use "nominal_dt_quot.ML"
-ML {* open Nominal_Dt_Quot *}
-
-
-end