| changeset 40652 | 7bdfc1d6b143 |
| parent 40651 | 9752ba7348b5 |
| child 40657 | 58a6ba7ccfc5 |
--- a/src/HOL/Enum.thy Mon Nov 22 11:34:57 2010 +0100 +++ b/src/HOL/Enum.thy Mon Nov 22 11:34:58 2010 +0100 @@ -69,6 +69,9 @@ lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum" by (simp add: list_ex_iff enum_all) +lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum" +unfolding list_ex1_iff enum_all by auto + subsection {* Default instances *}