184   asm_full_simp_tac (HOL_ss addsimps 

   184   asm_full_simp_tac (HOL_ss addsimps 

   185     @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW

   185     @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW

   186   (split_conjs THEN_ALL_NEW TRY o resolve_tac

   186   (split_conjs THEN_ALL_NEW TRY o resolve_tac

   187     @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})

   187     @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})

   188   THEN_ALL_NEW

   188   THEN_ALL_NEW

   190 *}

   190 *}

   191 

   191 

   192 ML {*

   192 ML {*

   193 fun build_alpha_eqvt alpha names =

   193 fun build_alpha_eqvt alpha names =

   194 let

   194 let