equal
deleted
inserted
replaced
111 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
111 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
112 apply (simp_all add: alpha5_inj) |
112 apply (simp_all add: alpha5_inj) |
113 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
113 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
114 apply (simp_all add: alpha5_inj) |
114 apply (simp_all add: alpha5_inj) |
115 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) |
115 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) |
|
116 (* HERE *) |
116 apply (simp add: alpha_gen) |
117 apply (simp add: alpha_gen) |
117 apply clarify |
118 apply clarify |
118 apply(simp add: fresh_star_plus) |
119 apply(simp add: fresh_star_plus) |
119 apply (rule conjI) |
120 apply (rule conjI) |
120 apply (erule_tac x="- pi \<bullet> rltsaa" in allE) |
121 apply (erule_tac x="- pi \<bullet> rltsaa" in allE) |