| changeset 10042 | 7164dc0d24d8 |
| parent 8116 | 759f712f8f06 |
| child 11026 | a50365d21144 |
| 10041:30693ebd16ae | 10042:7164dc0d24d8 |
|---|---|
8 |
8 |
9 JBasis = Main + |
9 JBasis = Main + |
10 |
10 |
11 constdefs |
11 constdefs |
12 |
12 |
13 unique :: "('a \\<times> 'b) list \\<Rightarrow> bool" |
13 unique :: "('a \\<times> 'b) list => bool" |
14 "unique \\<equiv> nodups \\<circ> map fst" |
14 "unique == nodups \\<circ> map fst" |
15 |
15 |
16 end |
16 end |