# HG changeset patch
# User bulwahn
# Date 1327928120 -3600
# Node ID 2795607a1f4009d939631cb7c68f9f91dafade31
# Parent  48fcca8965f4e4aad164a5facc7ca2c15e96838d
adding code equation for tranclp

diff -r 48fcca8965f4 -r 2795607a1f40 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Mon Jan 30 13:55:19 2012 +0100
+++ b/src/HOL/Enum.thy	Mon Jan 30 13:55:20 2012 +0100
@@ -787,6 +787,9 @@
   "Collect P = set (filter P enum)"
 by (auto simp add: enum_UNIV)
 
+lemma tranclp_unfold [code, no_atp]:
+  "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
+by (simp add: trancl_def)
 
 subsection {* Executable accessible part *}
 (* FIXME: should be moved somewhere else !? *)