equal
deleted
inserted
replaced
179 apply (simp add: fresh_star_def pure_fresh) |
179 apply (simp add: fresh_star_def pure_fresh) |
180 apply (simp add: fresh_star_def pure_fresh) |
180 apply (simp add: fresh_star_def pure_fresh) |
181 apply (simp add: eqvt_at_def) |
181 apply (simp add: eqvt_at_def) |
182 apply (simp add: eqvt_at_def) |
182 apply (simp add: eqvt_at_def) |
183 --"" |
183 --"" |
|
184 apply(simp_all add: eqvt_def inj_on_def) |
|
185 apply(perm_simp) |
|
186 apply(simp) |
|
187 apply(perm_simp) |
|
188 apply(simp) |
184 done |
189 done |
185 |
190 |
186 termination by lexicographic_order |
191 termination by lexicographic_order |
187 |
192 |
188 end |
193 end |