equal
deleted
inserted
replaced
631 fixes pi1 :: "'x prm" |
631 fixes pi1 :: "'x prm" |
632 and pi2 :: "'x prm" |
632 and pi2 :: "'x prm" |
633 assumes at: "at TYPE('x)" |
633 assumes at: "at TYPE('x)" |
634 shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)" |
634 shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)" |
635 by (simp add: at_prm_rev_eq[OF at]) |
635 by (simp add: at_prm_rev_eq[OF at]) |
636 |
|
637 lemma at_perm_fresh_fresh: |
|
638 fixes a :: "'x" |
|
639 assumes |
|
640 |
636 |
641 |
637 |
642 lemma at_ds1: |
638 lemma at_ds1: |
643 fixes a :: "'x" |
639 fixes a :: "'x" |
644 assumes at: "at TYPE('x)" |
640 assumes at: "at TYPE('x)" |