--- a/Nominal/Ex/SingleLet.thy	Wed May 26 15:37:56 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Thu May 27 18:37:52 2010 +0200
@@ -23,9 +23,40 @@
   "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 empty_eqvt[eqvt]:
+  shows "p \<bullet> {} = {}"
+  unfolding empty_def
+  by (perm_simp) (rule refl)
+*)
+lemma 
+  "(p \<bullet> {}) = {}"
+thm eqvts_raw
+thm eqvts
+apply(perm_strict_simp)
+
+
+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(simp_all)
+apply(perm_simp)
+apply(rule refl)
+apply(perm_simp)
+apply(rule refl)
+apply(perm_simp)
+apply(rule refl)
+apply(simp add: fv_trm_raw.simps)
+
 
 
 ML {* Inductive.the_inductive *}