--- a/Nominal/Ex/ExLF.thy	Mon May 10 15:44:49 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +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
-
-end
-
-
-
-