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