--- a/Quot/Nominal/Terms.thy	Mon Feb 22 18:09:44 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 23 09:31:59 2010 +0100
@@ -120,29 +120,6 @@
   (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}
 thm alpha1_equivp
 
-(*prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
-by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *})
-
-prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
-by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *})
-
-prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
-by (tactic {* transp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *})
-
-lemma alpha1_equivp:
-  "equivp alpha_rtrm1"
-  "equivp alpha_bp"
-apply (tactic {*
-  (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
-  THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN'
-  resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux})
-  THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN'
-  resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux}
-  THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux})
-)
-1 *})
-done*)
-
 quotient_type trm1 = rtrm1 / alpha_rtrm1
   by (rule alpha1_equivp(1))
 
@@ -227,12 +204,8 @@
 lemma bp_supp: "finite (supp (bp :: bp))"
   apply (induct bp)
   apply(simp_all add: supp_def)
-  apply (fold supp_def)
-  apply (simp add: supp_at_base)
-  apply(simp add: Collect_imp_eq)
-  apply(simp add: Collect_neg_eq[symmetric])
-  apply (fold supp_def)
-  apply (simp)
+  apply(simp add: supp_at_base supp_def[symmetric])
+  apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric] supp_def)
   done
 
 instance trm1 :: fs
@@ -459,24 +432,14 @@
   "a \<approx>4l b \<Longrightarrow> (pi \<bullet> a) \<approx>4l (pi \<bullet> b)"
 sorry
 
-(*
-prove alpha4_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] ("x","y","z")) *}
-apply (tactic {* 
-transp_tac @{thm rtrm4.induct} @{thms alpha4_inj} @{thms rtrm4.inject list.inject} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha1_eqvt} 1 *})
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
-  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases list.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
-*)
-
-
-
-
-lemma alpha4_equivp: "equivp alpha_rtrm4" sorry
-lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry
+  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
+thm alpha4_equivp
 
 quotient_type 
   qrtrm4 = rtrm4 / alpha_rtrm4 and
   qrtrm4list = "rtrm4 list" / alpha_rtrm4_list
-  by (simp_all add: alpha4_equivp alpha4list_equivp)
+  by (simp_all add: alpha4_equivp)
 
 
 datatype rtrm5 =