--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/LF.thy	Sun May 09 12:38:59 2010 +0100
@@ -0,0 +1,35 @@
+theory LF
+imports "../NewParser"
+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
+
+declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
+
+
+end
+
+
+
+