| changeset 35416 | d8d7d1b785af |
| parent 24783 | 5a3e336a2e37 |
| child 41589 | bbd861837ebc |
--- a/src/HOL/MicroJava/J/JBasis.thy Wed Feb 24 11:55:52 2010 +0100 +++ b/src/HOL/MicroJava/J/JBasis.thy Mon Mar 01 13:40:23 2010 +0100 @@ -15,8 +15,7 @@ section "unique" -constdefs - unique :: "('a \<times> 'b) list => bool" +definition unique :: "('a \<times> 'b) list => bool" where "unique == distinct \<circ> map fst"