--- a/src/HOL/Library/Transitive_Closure_Table.thy Fri May 09 08:13:28 2014 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Fri May 09 08:13:36 2014 +0200
@@ -190,29 +190,4 @@
code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
-subsection {* A simple example *}
-
-datatype ty = A | B | C
-
-inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
-where
- "test A B"
-| "test B A"
-| "test B C"
-
-subsubsection {* Invoking with the predicate compiler and the generic code generator *}
-
-code_pred test .
-
-values "{x. test\<^sup>*\<^sup>* A C}"
-values "{x. test\<^sup>*\<^sup>* C A}"
-values "{x. test\<^sup>*\<^sup>* A x}"
-values "{x. test\<^sup>*\<^sup>* x C}"
-
-value "test\<^sup>*\<^sup>* A C"
-value "test\<^sup>*\<^sup>* C A"
-
-hide_type ty
-hide_const test A B C
-
end
\ No newline at end of file
--- a/src/HOL/ROOT Fri May 09 08:13:28 2014 +0200
+++ b/src/HOL/ROOT Fri May 09 08:13:36 2014 +0200
@@ -518,6 +518,7 @@
Serbian
"~~/src/HOL/Library/FinFun_Syntax"
"~~/src/HOL/Library/Refute"
+ "~~/src/HOL/Library/Transitive_Closure_Table"
Cartouche_Examples
theories
Iff_Oracle
@@ -560,6 +561,7 @@
Sqrt_Script
Transfer_Ex
Transfer_Int_Nat
+ Transitive_Closure_Table_Ex
HarmonicSeries
Refute_Examples
Execute_Choice
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy Fri May 09 08:13:36 2014 +0200
@@ -0,0 +1,30 @@
+(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
+
+header {* Simple example for table-based implementation of the reflexive transitive closure *}
+
+theory Transitive_Closure_Table_Ex
+imports "~~/src/HOL/Library/Transitive_Closure_Table"
+begin
+
+datatype ty = A | B | C
+
+inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
+where
+ "test A B"
+| "test B A"
+| "test B C"
+
+
+text {* Invoking with the predicate compiler and the generic code generator *}
+
+code_pred test .
+
+values "{x. test\<^sup>*\<^sup>* A C}"
+values "{x. test\<^sup>*\<^sup>* C A}"
+values "{x. test\<^sup>*\<^sup>* A x}"
+values "{x. test\<^sup>*\<^sup>* x C}"
+
+value "test\<^sup>*\<^sup>* A C"
+value "test\<^sup>*\<^sup>* C A"
+
+end