| changeset 46783 | 3e89a5cab8d7 |
| parent 44890 | 22f665a2e91c |
| child 50134 | 13211e07d931 |
| 46782:d50855d9ea74 | 46783:3e89a5cab8d7 |
|---|---|
587 |
587 |
588 lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x" |
588 lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x" |
589 by (simp add: atmost_one_def) |
589 by (simp add: atmost_one_def) |
590 |
590 |
591 end |
591 end |
592 |