--- a/Nominal/Ex/LF.thy	Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/LF.thy	Wed Dec 22 09:13:25 2010 +0000
@@ -2,25 +2,40 @@
 imports "../Nominal2"
 begin
 
-declare [[STEPS = 100]]
-
 atom_decl name
 atom_decl ident
 
-nominal_datatype kind =
-    Type
-  | KPi "ty" n::"name" k::"kind" bind n in k
+nominal_datatype lf:
+    kind =
+      Type
+    | KPi "ty" n::"name" k::"kind" bind n in k
 and ty =
-    TConst "ident"
-  | TApp "ty" "trm"
-  | TPi "ty" n::"name" ty::"ty"   bind n in ty
+      TConst "ident"
+    | TApp "ty" "trm"
+    | TPi "ty" n::"name" ty::"ty"   bind n in ty
 and trm =
-    Const "ident"
-  | Var "name"
-  | App "trm" "trm"
-  | Lam "ty" n::"name" t::"trm"  bind n in t
+      Const "ident"
+    | Var "name"
+    | App "trm" "trm"
+    | Lam "ty" n::"name" t::"trm"  bind n in t
 
-(*thm kind_ty_trm.supp*)
+thm lf.distinct
+thm lf.induct
+thm lf.inducts
+thm lf.exhaust
+thm lf.strong_exhaust
+thm lf.fv_defs
+thm lf.bn_defs
+thm lf.perm_simps
+thm lf.eq_iff
+thm lf.fv_bn_eqvt
+thm lf.size_eqvt
+thm lf.supports
+thm lf.fsupp
+thm lf.supp
+thm lf.fresh
+thm lf.fresh[simplified]
+
 
 
 end