improving the setup for the tabled transitive closure thanks to usage of Andreas Lochbihler
authorbulwahn
Mon, 23 Nov 2009 19:42:52 +0100
changeset 33870 5b0d23d2c08f
parent 33866 34e45b2afe43
child 33871 caab5399bb2d
improving the setup for the tabled transitive closure thanks to usage of Andreas Lochbihler
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