--- a/Nominal/Ex/Classical.thy	Wed Aug 25 20:19:10 2010 +0800
+++ b/Nominal/Ex/Classical.thy	Wed Aug 25 22:55:42 2010 +0800
@@ -7,7 +7,7 @@
 atom_decl name
 atom_decl coname
 
-declare [[STEPS = 9]]
+declare [[STEPS = 21]]
 
 nominal_datatype trm =
    Ax "name" "coname"
@@ -18,17 +18,17 @@
 |  ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"       bind c in t1, bind n in t2
 |  ImpR c::"coname" n::"name" t::"trm" "coname"                bind n c in t
 
-thm alpha_trm_raw.intros[no_vars]
+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 trm.fv
-thm trm.eq_iff
-thm trm.bn
-thm trm.perm
-thm trm.induct
-thm trm.distinct
-thm trm.fv[simplified trm.supp]
-*)
+
 
 
 end