46   using [[simproc del: alpha_lst]]

    46   using [[simproc del: alpha_lst]]

    47   apply auto

    47   apply auto

    48   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)

    48   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)

    49   using [[simproc del: alpha_lst]]

    49   using [[simproc del: alpha_lst]]

    50   apply (auto simp add: fresh_star_def)

    50   apply (auto simp add: fresh_star_def)

    52   apply (erule Abs_lst1_fcb)

    51   apply (erule Abs_lst1_fcb)

    53   apply (simp_all add: Abs_fresh_iff)

    52   apply (simp_all add: Abs_fresh_iff)

    54   apply (erule fresh_eqvt_at)

    53   apply (erule fresh_eqvt_at)

    55   apply (simp add: finite_supp)

    54   apply (simp add: finite_supp)

    56   apply (simp add: fresh_Pair)

    55   apply (simp add: fresh_Pair)

    80   defer

    79   defer

    81   apply (case_tac x)

    80   apply (case_tac x)

    82   apply (rule_tac y="a" in lt.exhaust)

    81   apply (rule_tac y="a" in lt.exhaust)

    83   using [[simproc del: alpha_lst]]

    82   using [[simproc del: alpha_lst]]

    84   apply auto

    83   apply auto

    86   apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)

    84   apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)

    87   apply (simp add: Abs1_eq_iff)

    85   apply (simp add: Abs1_eq_iff)

    88   apply blast+

    86   apply blast+

    89   apply (rule_tac y="b" in lt.exhaust)

    87   apply (rule_tac y="b" in lt.exhaust)

    90   apply auto

    88   apply auto