equal
deleted
inserted
replaced
135 fixes a b::"'a::at" |
135 fixes a b::"'a::at" |
136 shows "(a \<leftrightarrow> b) \<bullet> a = b" |
136 shows "(a \<leftrightarrow> b) \<bullet> a = b" |
137 and "(a \<leftrightarrow> b) \<bullet> b = a" |
137 and "(a \<leftrightarrow> b) \<bullet> b = a" |
138 unfolding permute_flip_at by simp_all |
138 unfolding permute_flip_at by simp_all |
139 |
139 |
|
140 lemma flip_fresh_fresh: |
|
141 fixes a b::"'a::at_base" |
|
142 assumes "atom a \<sharp> x" "atom b \<sharp> x" |
|
143 shows "(a \<leftrightarrow> b) \<bullet> x = x" |
|
144 using assms |
|
145 by (simp add: flip_def swap_fresh_fresh) |
140 |
146 |
141 subsection {* Syntax for coercing at-elements to the atom-type *} |
147 subsection {* Syntax for coercing at-elements to the atom-type *} |
142 |
148 |
143 (* |
149 (* |
144 syntax |
150 syntax |