--- a/Nominal/LFex.thy	Tue Mar 23 09:21:43 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-theory LFex
-imports "Parser"
-begin
-
-atom_decl name
-atom_decl ident
-
-nominal_datatype kind =
-    Type
-  | KPi "ty" n::"name" k::"kind" bind n in k
-and ty =
-    TConst "ident"
-  | TApp "ty" "trm"
-  | TPi "ty" n::"name" t::"ty" bind n in t
-and trm =
-    Const "ident"
-  | Var "name"
-  | App "trm" "trm"
-  | Lam "ty" n::"name" t::"trm" bind n in t
-
-thm kind_ty_trm.supp
-
-end
-
-
-
-