--- a/Nominal/Ex/ExLF.thy	Sun May 09 12:26:10 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-theory ExLF
-imports "../NewParser"
-begin
-
-atom_decl name
-atom_decl ident
-
-nominal_datatype kind =
-    Type
-  | KPi "ty" n::"name" k::"kind" bind_set n in k
-and ty =
-    TConst "ident"
-  | TApp "ty" "trm"
-  | TPi "ty" n::"name" t::"ty" bind_set n in t
-and trm =
-    Const "ident"
-  | Var "name"
-  | App "trm" "trm"
-  | Lam "ty" n::"name" t::"trm" bind_set n in t
-
-thm kind_ty_trm.supp
-
-declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
-
-equivariance alpha_trm_raw
-
-
-
-
-end
-
-
-
-