equal
deleted
inserted
replaced
59 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
59 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
60 apply (simp add: pure_supp fresh_star_def) |
60 apply (simp add: pure_supp fresh_star_def) |
61 apply(simp add: eqvt_at_def) |
61 apply(simp add: eqvt_at_def) |
62 done |
62 done |
63 |
63 |
64 termination (eqvt) by lexicographic_order |
64 nominal_termination (eqvt) by lexicographic_order |
65 |
65 |
66 thm height_trm_height_bp.eqvt |
66 thm height_trm_height_bp.eqvt |
67 |
67 |
68 |
68 |
69 end |
69 end |