src/HOL/Transitive_Closure.thy

--- a/src/HOL/Transitive_Closure.thy	Thu Jan 05 20:26:01 2012 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sun Jan 01 11:28:45 2012 +0100
@@ -1047,7 +1047,7 @@
 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   "acyclicP r \<equiv> acyclic {(x, y). r x y}"
 
-lemma acyclic_irrefl:
+lemma acyclic_irrefl [code]:
   "acyclic r \<longleftrightarrow> irrefl (r^+)"
   by (simp add: acyclic_def irrefl_def)