src/HOL/Library/Transitive_Closure_Table.thy
changeset 46359 9bc43dc49d0a
parent 45231 d85a2fdc586c
child 55419 8b7c7157fa11
--- 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