--- a/Nominal/Ex/Multi_Recs2.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -49,6 +49,54 @@
 | "b_lrb (Clause fcs) = (b_fnclauses fcs)"
 | "b_fnclause (K x pat exp) = {atom x}"
 
+
+
+thm fun_recs.perm_bn_alpha
+thm fun_recs.perm_bn_simps
+thm fun_recs.bn_finite
+thm fun_recs.inducts
+thm fun_recs.distinct
+thm fun_recs.induct
+thm fun_recs.inducts
+thm fun_recs.exhaust
+thm fun_recs.fv_defs
+thm fun_recs.bn_defs
+thm fun_recs.perm_simps
+thm fun_recs.eq_iff
+thm fun_recs.fv_bn_eqvt
+thm fun_recs.size_eqvt
+thm fun_recs.supports
+thm fun_recs.fsupp
+thm fun_recs.supp
+
+term alpha_b_fnclause
+term alpha_b_fnclauses
+term alpha_b_lrb
+term alpha_b_lrbs
+term alpha_b_pat
+
+term alpha_b_fnclause_raw
+term alpha_b_fnclauses_raw
+term alpha_b_lrb_raw
+term alpha_b_lrbs_raw
+term alpha_b_pat_raw
+
+lemma uu1:
+  fixes as0::exp  and as1::fnclause
+  shows "(\<lambda>x::exp. True) (as0::exp)"
+  and   "alpha_b_fnclause as1 (permute_b_fnclause p as1)"
+  and   "alpha_b_fnclauses as2 (permute_b_fnclauses p as2)"
+  and   "alpha_b_lrb as3 (permute_b_lrb p as3)"
+  and   "alpha_b_lrbs as4 (permute_b_lrbs p as4)"
+  and   "alpha_b_pat as5 (permute_b_pat p as5)"
+apply(induct as0 and as1 and as2 and as3 and as4 and as5 rule: fun_recs.inducts)
+apply(simp_all)
+apply(simp only: fun_recs.perm_bn_simps)
+apply(simp only: fun_recs.eq_iff)
+apply(simp)
+oops
+
+
 thm fun_recs.distinct
 thm fun_recs.induct
 thm fun_recs.inducts