diff -r 339a8b3c4791 -r b2eb87bd541b src/HOL/Enum.thy --- a/src/HOL/Enum.thy Thu Oct 13 23:27:46 2011 +0200 +++ b/src/HOL/Enum.thy Thu Oct 13 23:35:15 2011 +0200 @@ -759,11 +759,10 @@ qed -subsection {* An executable card operator on finite types *} +subsection {* Transitive closure on relations over finite types *} -lemma [code]: - "card R = length (filter R enum)" - by (simp add: distinct_length_filter [OF enum_distinct] enum_UNIV Collect_def) +lemma [code]: "trancl (R :: (('a :: enum) \ 'a) set) = ntrancl (length (filter R enum) - 1) R" + by (simp add: finite_trancl_ntranl distinct_length_filter [OF enum_distinct] enum_UNIV Collect_def) subsection {* Closing up *}