equal
deleted
inserted
replaced
1833 |
1833 |
1834 lemma fresh_at_base: |
1834 lemma fresh_at_base: |
1835 shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b" |
1835 shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b" |
1836 unfolding fresh_def by (simp add: supp_at_base) |
1836 unfolding fresh_def by (simp add: supp_at_base) |
1837 |
1837 |
|
1838 lemma fresh_atom_at_base: |
|
1839 fixes b::"'a::at_base" |
|
1840 shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b" |
|
1841 by (simp add: fresh_def supp_at_base supp_atom) |
|
1842 |
|
1843 |
1838 instance at_base < fs |
1844 instance at_base < fs |
1839 proof qed (simp add: supp_at_base) |
1845 proof qed (simp add: supp_at_base) |
1840 |
1846 |
1841 lemma at_base_infinite [simp]: |
1847 lemma at_base_infinite [simp]: |
1842 shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U") |
1848 shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U") |