# HG changeset patch
# User haftmann
# Date 1318541715 -7200
# Node ID b2eb87bd541b99f1eafc42d90bad5ccc90dfdc6b
# Parent  339a8b3c479197d6be767da24f90db7f684e6c8e
avoid very specific code equation for card; corrected spelling

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) \<times> '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 *}
diff -r 339a8b3c4791 -r b2eb87bd541b src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Oct 13 23:27:46 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Oct 13 23:35:15 2011 +0200
@@ -1034,13 +1034,10 @@
     unfolding ntrancl_def by fastforce
 qed
 
-lemma finnite_trancl_ntranl:
+lemma finite_trancl_ntranl:
   "finite R \<Longrightarrow> trancl R = ntrancl (card R - 1) R"
   by (cases "card R") (auto simp add: trancl_finite_eq_rel_pow rel_pow_empty ntrancl_def)
 
-lemma [code]: "trancl (R :: (('a :: finite) \<times> 'a) set) = ntrancl (card R - 1) R"
-  by (simp add: finnite_trancl_ntranl)
-
 
 subsection {* Acyclic relations *}