diff -r 6d46f7ea1661 -r 06bf338e3215 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Wed Jun 29 13:04:24 2011 +0900
+++ b/Nominal/Ex/Let.thy	Wed Jun 29 16:44:54 2011 +0100
@@ -18,8 +18,16 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
+print_theorems
+
+thm alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros
+thm bn_raw.simps
+thm permute_bn_raw.simps
+thm trm_assn.perm_bn_alpha
+thm trm_assn.permute_bn
+
 thm trm_assn.fv_defs
-thm trm_assn.eq_iff
+thm trm_assn.eq_iff 
 thm trm_assn.bn_defs
 thm trm_assn.bn_inducts
 thm trm_assn.perm_simps
@@ -117,9 +125,17 @@
   apply (simp add: alphas trm_assn.supp supp_at_base x y fresh_star_def atom_eqvt)
   by (metis Rep_name_inverse atom_name_def flip_fresh_fresh fresh_atom fresh_perm x y)
 
+
 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
   by (simp add: permute_pure)
 
+(* TODO: should be provided by nominal *)
+lemmas [eqvt] = trm_assn.fv_bn_eqvt
+thm trm_assn.fv_bn_eqvt
+
+
+thm Abs_lst_fcb
+
 lemma Abs_lst_fcb2:
   fixes as bs :: "'a :: fs"
     and x y :: "'b :: fs"
@@ -131,7 +147,7 @@
   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
   and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
 (* What we would like in this proof, and lets this proof finish *)
-  and bainj: "\<And>q r. q \<bullet> ba as = r \<bullet> ba bs \<Longrightarrow> q \<bullet> as = r \<bullet> bs"
+  and ba_inj: "\<And>q r. q \<bullet> ba as = r \<bullet> ba bs \<Longrightarrow> q \<bullet> as = r \<bullet> bs"
 (* What the user can supply with the help of alpha_bn *)
 (*  and bainj: "ba as = ba bs \<Longrightarrow> as = bs"*)
   shows "f as x c = f bs y c"
@@ -178,7 +194,7 @@
     using inc fresh1 fr1
     apply(auto simp add: fresh_star_def fresh_Pair)
     done
-  then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 bainj 
+  then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 ba_inj 
     by simp
   then have "r \<bullet> ((set (ba bs)) \<sharp>* f bs y c)"
     apply(simp add: fresh_star_eqvt set_eqvt)
@@ -193,7 +209,7 @@
   also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c"
     apply(rule perm1)
     using inc fresh1 fr1 by (auto simp add: fresh_star_def)
-  also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 bainj by simp
+  also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 ba_inj by simp
   also have "\<dots> = r \<bullet> (f bs y c)"
     apply(rule perm2[symmetric])
     using qq3 fresh2 fr1 by (auto simp add: fresh_star_def)