| changeset 2460 | 16d32eddc17f |
| parent 2447 | 76be909eaf04 |
| child 2467 | 67b3933c3190 |
| 2459:ac3470e1e5af | 2460:16d32eddc17f |
|---|---|
366 apply(simp_all) |
366 apply(simp_all) |
367 done |
367 done |
368 |
368 |
369 end |
369 end |
370 |
370 |
371 lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst |
371 lemmas permute_abs[eqvt] = permute_Abs permute_Abs_res permute_Abs_lst |
372 |
372 |
373 |
373 |
374 lemma abs_swap1: |
374 lemma abs_swap1: |
375 assumes a1: "a \<notin> (supp x) - bs" |
375 assumes a1: "a \<notin> (supp x) - bs" |
376 and a2: "b \<notin> (supp x) - bs" |
376 and a2: "b \<notin> (supp x) - bs" |