# HG changeset patch
# User bulwahn
# Date 1327928122 -3600
# Node ID 9bc43dc49d0a4566583a603c8252294925096c28
# Parent  b2a93648668511dd64c2f8fcaa76b9c78c05759a
adding code equation for rtranclp in Enum

diff -r b2a936486685 -r 9bc43dc49d0a src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Mon Jan 30 13:55:21 2012 +0100
+++ b/src/HOL/Enum.thy	Mon Jan 30 13:55:22 2012 +0100
@@ -791,6 +791,10 @@
   "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
 by (simp add: trancl_def)
 
+lemma rtranclp_rtrancl_eq[code, no_atp]:
+  "rtranclp r x y = ((x, y) : rtrancl {(x, y). r x y})"
+unfolding rtrancl_def by auto
+
 lemma max_ext_eq[code]:
   "max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X --> (EX xa : Y. (x, xa) : R))}"
 by (auto simp add: max_ext.simps)
diff -r b2a936486685 -r 9bc43dc49d0a src/HOL/Library/Transitive_Closure_Table.thy
--- a/src/HOL/Library/Transitive_Closure_Table.thy	Mon Jan 30 13:55:21 2012 +0100
+++ b/src/HOL/Library/Transitive_Closure_Table.thy	Mon Jan 30 13:55:22 2012 +0100
@@ -185,6 +185,7 @@
     by (auto simp add: rtranclp_eq_rtrancl_path)
 qed
 
+declare rtranclp_rtrancl_eq[code del]
 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
 
 code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
@@ -214,5 +215,4 @@
 hide_type ty
 hide_const test A B C
 
-end
-
+end
\ No newline at end of file