equal
deleted
inserted
replaced
10 |
10 |
11 consts |
11 consts |
12 perm :: "('a list * 'a list) set" |
12 perm :: "('a list * 'a list) set" |
13 |
13 |
14 abbreviation |
14 abbreviation |
15 perm_rel :: "'a list => 'a list => bool" ("_ <~~> _" [50, 50] 50) |
15 perm_rel :: "'a list => 'a list => bool" ("_ <~~> _" [50, 50] 50) where |
16 "x <~~> y == (x, y) \<in> perm" |
16 "x <~~> y == (x, y) \<in> perm" |
17 |
17 |
18 inductive perm |
18 inductive perm |
19 intros |
19 intros |
20 Nil [intro!]: "[] <~~> []" |
20 Nil [intro!]: "[] <~~> []" |