--- 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 *}