--- a/Nominal/Ex/SingleLet.thy	Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -4,9 +4,9 @@
 
 atom_decl name
 
-declare [[STEPS = 21]]
+declare [[STEPS = 100]]
 
-nominal_datatype singlelet: trm  =
+nominal_datatype single_let: trm  =
   Var "name"
 | App "trm" "trm"
 | Lam x::"name" t::"trm"  bind x in t
@@ -21,19 +21,18 @@
 where
   "bn (As x y t) = {atom x}"
 
-
-thm distinct
-thm induct
-thm exhaust
-thm fv_defs
-thm bn_defs
-thm perm_simps
-thm eq_iff
-thm fv_bn_eqvt
-thm size_eqvt
+thm single_let.distinct
+thm single_let.induct
+thm single_let.exhaust
+thm single_let.fv_defs
+thm single_let.bn_defs
+thm single_let.perm_simps
+thm single_let.eq_iff
+thm single_let.fv_bn_eqvt
+thm single_let.size_eqvt
 
 
-
+(*
 
 
 lemma supp_fv:
@@ -67,10 +66,9 @@
 thm trm_assg.inducts
 thm trm_assg.distinct
 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
+*)
 
-(* TEMPORARY
-thm trm_assg.fv[simplified trm_assg.supp(1-2)]
-*)
+
 
 end