| changeset 1317 | a8627c3bdd0c |
| parent 1312 | b0eae8c93314 |
| child 1327 | 670701b19e8e |
| 1316:0577afdb1732 | 1317:a8627c3bdd0c |
|---|---|
498 apply(case_tac "a = b") |
498 apply(case_tac "a = b") |
499 apply(simp) |
499 apply(simp) |
500 oops |
500 oops |
501 |
501 |
502 *) |
502 *) |
503 |
|
504 fun |
|
505 distinct_perms |
|
506 where |
|
507 "distinct_perms [] = True" |
|
508 | "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)" |
|
509 |
|
510 |
|
511 |
|
503 end |
512 end |
504 |
513 |