equal
deleted
inserted
replaced
659 apply(rule TrueI) |
659 apply(rule TrueI) |
660 apply (case_tac x) |
660 apply (case_tac x) |
661 apply (case_tac a rule: lam.exhaust) |
661 apply (case_tac a rule: lam.exhaust) |
662 using [[simproc del: alpha_lst]] |
662 using [[simproc del: alpha_lst]] |
663 apply simp_all[3] |
663 apply simp_all[3] |
664 apply blast |
|
665 apply (case_tac b) |
664 apply (case_tac b) |
666 apply (rule_tac y="a" and c="ba" in lam.strong_exhaust) |
665 apply (rule_tac y="a" and c="ba" in lam.strong_exhaust) |
667 apply simp_all[3] |
666 apply simp_all[3] |
668 apply blast |
|
669 apply blast |
|
670 apply (simp add: Abs1_eq_iff fresh_star_def) |
667 apply (simp add: Abs1_eq_iff fresh_star_def) |
671 using [[simproc del: alpha_lst]] |
668 using [[simproc del: alpha_lst]] |
672 apply(simp_all) |
669 apply(simp_all) |
673 apply(erule_tac c="()" in Abs_lst1_fcb2) |
670 apply(erule_tac c="()" in Abs_lst1_fcb2) |
674 apply (simp add: Abs_fresh_iff) |
671 apply (simp add: Abs_fresh_iff) |
711 apply (rule TrueI) |
708 apply (rule TrueI) |
712 apply (case_tac x) |
709 apply (case_tac x) |
713 apply (rule_tac y="a" in lam.exhaust) |
710 apply (rule_tac y="a" in lam.exhaust) |
714 using [[simproc del: alpha_lst]] |
711 using [[simproc del: alpha_lst]] |
715 apply simp_all |
712 apply simp_all |
716 apply blast |
|
717 apply blast |
|
718 apply (rule_tac x="(name, lam)" and ?'a="name" in obtain_fresh) |
713 apply (rule_tac x="(name, lam)" and ?'a="name" in obtain_fresh) |
719 apply blast |
714 apply blast |
720 apply clarify |
715 apply clarify |
721 apply (rule_tac x="(x, xa, M, Ma, c, ca, Na)" and ?'a="name" in obtain_fresh) |
716 apply (rule_tac x="(x, xa, M, Ma, c, ca, Na)" and ?'a="name" in obtain_fresh) |
722 apply (subgoal_tac "eqvt_at q_sumC (Var ca, Na)") --"Could come from nominal_function?" |
717 apply (subgoal_tac "eqvt_at q_sumC (Var ca, Na)") --"Could come from nominal_function?" |