changeset 22473 | 753123c89d72 |
parent 22384 | 33a46e6c7f04 |
child 22492 | 43545e640877 |
--- a/src/HOL/ex/CodeCollections.thy Mon Mar 19 19:28:27 2007 +0100 +++ b/src/HOL/ex/CodeCollections.thy Tue Mar 20 08:27:15 2007 +0100 @@ -74,7 +74,7 @@ "list_ex P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)" by (induct xs) auto -class finite = +class finite = type + fixes fin :: "'a list" assumes member_fin: "x \<in> set fin" begin