--- a/Nominal/Term5.thy	Tue Mar 16 12:06:22 2010 +0100
+++ b/Nominal/Term5.thy	Tue Mar 16 12:08:37 2010 +0100
@@ -57,16 +57,20 @@
 lemma alpha5_reflp:
 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)"
 apply (rule rtrm5_rlts.induct)
+thm rtrm5_rlts.induct
+ alpha_rtrm5_alpha_rlts_alpha_rbv5.induct
 apply (simp_all add: alpha5_inj)
 apply (rule_tac x="0::perm" in exI)
 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm)
 done
 
 lemma alpha5_symp:
-"(a \<approx>5 b \<longrightarrow> a \<approx>5 b) \<and>
+"(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)"
 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
+thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct
+thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros
 apply (simp_all add: alpha5_inj)
 sorry