| changeset 66453 | cc19f7ca2ed6 |
| parent 63882 | 018998c00003 |
| child 67226 | ec32cdaab97b |
| 66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
|---|---|
1 (* Author: Florian Haftmann, TU Muenchen *) |
1 (* Author: Florian Haftmann, TU Muenchen *) |
2 |
2 |
3 section \<open>Fragments on permuations\<close> |
3 section \<open>Fragments on permuations\<close> |
4 |
4 |
5 theory Perm_Fragments |
5 theory Perm_Fragments |
6 imports "~~/src/HOL/Library/Perm" "~~/src/HOL/Library/Dlist" |
6 imports "HOL-Library.Perm" "HOL-Library.Dlist" |
7 begin |
7 begin |
8 |
8 |
9 unbundle permutation_syntax |
9 unbundle permutation_syntax |
10 |
10 |
11 |
11 |