# HG changeset patch
# User bulwahn
# Date 1259001772 -3600
# Node ID 5b0d23d2c08f1a5a2fe315b11252feed88966926
# Parent  34e45b2afe43c10e3809884caf99f79b2d7d11eb
improving the setup for the tabled transitive closure thanks to usage of Andreas Lochbihler

diff -r 34e45b2afe43 -r 5b0d23d2c08f src/HOL/Library/Transitive_Closure_Table.thy
--- a/src/HOL/Library/Transitive_Closure_Table.thy	Mon Nov 23 19:03:16 2009 +0100
+++ b/src/HOL/Library/Transitive_Closure_Table.thy	Mon Nov 23 19:42:52 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