src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Tue Sep 20 15:23:17 2011 +0200
+++ b/src/HOL/Wellfounded.thy	Tue Sep 20 21:47:52 2011 +0200
@@ -387,6 +387,10 @@
 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   "acyclicP r == acyclic {(x, y). r x y}"
 
+lemma acyclic_irrefl:
+  "acyclic r \<longleftrightarrow> irrefl (r^+)"
+  by (simp add: acyclic_def irrefl_def)
+
 lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
   by (simp add: acyclic_def)