equal
deleted
inserted
replaced
5 section \<open>Permuted Lists\<close> |
5 section \<open>Permuted Lists\<close> |
6 |
6 |
7 theory List_Permutation |
7 theory List_Permutation |
8 imports Permutations |
8 imports Permutations |
9 begin |
9 begin |
|
10 |
|
11 text \<open> |
|
12 Note that multisets already provide the notion of permutated list and hence |
|
13 this theory mostly echoes material already logically present in theory |
|
14 \<^text>\<open>Permutations\<close>; it should be seldom needed. |
|
15 \<close> |
10 |
16 |
11 subsection \<open>An inductive definition \ldots\<close> |
17 subsection \<open>An inductive definition \ldots\<close> |
12 |
18 |
13 inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixr \<open><~~>\<close> 50) |
19 inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixr \<open><~~>\<close> 50) |
14 where |
20 where |