--- a/Nominal/Manual/Term5.thy	Fri Mar 26 17:22:17 2010 +0100
+++ b/Nominal/Manual/Term5.thy	Fri Mar 26 22:22:41 2010 +0100
@@ -1,5 +1,5 @@
 theory Term5
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+imports "../Nominal2_Atoms" "../Nominal2_Eqvt" "../Nominal2_Supp" "../Abs" "../Perm" "../Fv" "../Rsp"
 begin
 
 atom_decl name
@@ -23,7 +23,7 @@
 print_theorems
 
 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5")
-  [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *}
+  [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [(0,NONE), (2,SOME @{term rbv5})]])] *}
 print_theorems
 
 notation
@@ -31,7 +31,7 @@
   alpha_rlts ("_ \<approx>l _" [100, 100] 100)
 thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_rel_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *}
 thm alpha5_inj
 
 lemma rbv5_eqvt[eqvt]:
@@ -71,7 +71,17 @@
 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
-apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *})
+apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
+apply (simp_all add: alpha5_inj)
+apply (erule exE)
+apply (rule_tac x="-pi" in exI)
+apply (rule alpha_gen_sym)
+apply (simp_all add: alphas)
+apply (case_tac x)
+apply (case_tac y)
+apply (simp add: alpha5_eqvt)
+apply clarify
+apply simp
 done
 
 lemma alpha5_symp1: