# HG changeset patch
# User haftmann
# Date 1399616016 -7200
# Node ID d411a81b83564bc5eb4faca00f61fd7b2ea2ad5a
# Parent  5bf71b4da7067b8b73ba87e54fbbda8451b90e0f
removed junk from library theory

diff -r 5bf71b4da706 -r d411a81b8356 src/HOL/Library/Transitive_Closure_Table.thy
--- 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
diff -r 5bf71b4da706 -r d411a81b8356 src/HOL/ROOT
--- 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
diff -r 5bf71b4da706 -r d411a81b8356 src/HOL/ex/Transitive_Closure_Table_Ex.thy
--- /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