# HG changeset patch
# User bulwahn
# Date 1259009767 -3600
# Node ID caab5399bb2dd5bb86e4a909c225b37e05568c6f
# Parent  5b0d23d2c08f1a5a2fe315b11252feed88966926# Parent  0ec11efb9124b70d59f12f818d14e562b3a4c63d
merged

diff -r 0ec11efb9124 -r caab5399bb2d src/HOL/Library/Transitive_Closure_Table.thy
--- a/src/HOL/Library/Transitive_Closure_Table.thy	Mon Nov 23 21:24:15 2009 +0100
+++ b/src/HOL/Library/Transitive_Closure_Table.thy	Mon Nov 23 21:56:07 2009 +0100
@@ -185,7 +185,7 @@
     by (auto simp add: rtranclp_eq_rtrancl_path)
 qed
 
-declare rtranclp_eq_rtrancl_tab_nil [code_unfold]
+declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del]
 
 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
 
@@ -224,7 +224,11 @@
 values "{x. test\<^sup>*\<^sup>* A x}"
 values "{x. test\<^sup>*\<^sup>* x C}"
 
-hide const test
+value "test\<^sup>*\<^sup>* A C"
+value "test\<^sup>*\<^sup>* C A"
+
+hide type ty
+hide const test A B C
 
 end