--- a/Nominal/Ex/SingleLet.thy	Mon May 31 19:57:29 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Tue Jun 01 15:01:05 2010 +0200
@@ -24,23 +24,6 @@
 where
   "bn (As x t) = {atom x}"
 
-thm permute_trm_raw_permute_assg_raw.simps[no_vars]
-thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars]
-thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
-
-ML {* val {inducts, ... } = Function.get_info @{context} @{term "fv_trm_raw"}*}
-ML {* Rule_Cases.strict_mutual_rule @{context} (the inducts) *}
-
-lemma
- shows "p1 \<bullet> fv_trm_raw trm_raw = fv_trm_raw (p1 \<bullet> trm_raw)"
- and "p1 \<bullet> fv_assg_raw assg_raw = fv_assg_raw (p1 \<bullet> assg_raw)"
- and "p1 \<bullet> fv_bn_raw assg_raw = fv_bn_raw (p1 \<bullet> assg_raw)"
-apply(induct trm_raw and assg_raw and assg_raw rule: fv_trm_raw_fv_assg_raw_fv_bn_raw.induct)
-apply(perm_simp add: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps, rule refl)+
-done
-
-
-
 ML {* Inductive.the_inductive *}
 thm trm_assg.fv
 thm trm_assg.supp