src/HOL/Transitive_Closure.thy

   "acyclic r \<longleftrightarrow> (!x. (x,x) ~: r^+)"
 
 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)
 
 lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
   by (simp add: acyclic_def)