removed junk from library theory
authorhaftmann
Fri May 09 08:13:36 2014 +0200 (2014-05-09)
changeset 56922d411a81b8356
parent 56921 5bf71b4da706
child 56923 c062543d380e
removed junk from library theory
src/HOL/Library/Transitive_Closure_Table.thy
src/HOL/ROOT
src/HOL/ex/Transitive_Closure_Table_Ex.thy
     1.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Fri May 09 08:13:28 2014 +0200
     1.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Fri May 09 08:13:36 2014 +0200
     1.3 @@ -190,29 +190,4 @@
     1.4  
     1.5  code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
     1.6  
     1.7 -subsection {* A simple example *}
     1.8 -
     1.9 -datatype ty = A | B | C
    1.10 -
    1.11 -inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
    1.12 -where
    1.13 -  "test A B"
    1.14 -| "test B A"
    1.15 -| "test B C"
    1.16 -
    1.17 -subsubsection {* Invoking with the predicate compiler and the generic code generator *}
    1.18 -
    1.19 -code_pred test .
    1.20 -
    1.21 -values "{x. test\<^sup>*\<^sup>* A C}"
    1.22 -values "{x. test\<^sup>*\<^sup>* C A}"
    1.23 -values "{x. test\<^sup>*\<^sup>* A x}"
    1.24 -values "{x. test\<^sup>*\<^sup>* x C}"
    1.25 -
    1.26 -value "test\<^sup>*\<^sup>* A C"
    1.27 -value "test\<^sup>*\<^sup>* C A"
    1.28 -
    1.29 -hide_type ty
    1.30 -hide_const test A B C
    1.31 -
    1.32  end
    1.33 \ No newline at end of file
     2.1 --- a/src/HOL/ROOT	Fri May 09 08:13:28 2014 +0200
     2.2 +++ b/src/HOL/ROOT	Fri May 09 08:13:36 2014 +0200
     2.3 @@ -518,6 +518,7 @@
     2.4      Serbian
     2.5      "~~/src/HOL/Library/FinFun_Syntax"
     2.6      "~~/src/HOL/Library/Refute"
     2.7 +    "~~/src/HOL/Library/Transitive_Closure_Table"
     2.8      Cartouche_Examples
     2.9    theories
    2.10      Iff_Oracle
    2.11 @@ -560,6 +561,7 @@
    2.12      Sqrt_Script
    2.13      Transfer_Ex
    2.14      Transfer_Int_Nat
    2.15 +    Transitive_Closure_Table_Ex
    2.16      HarmonicSeries
    2.17      Refute_Examples
    2.18      Execute_Choice
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Fri May 09 08:13:36 2014 +0200
     3.3 @@ -0,0 +1,30 @@
     3.4 +(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
     3.5 +
     3.6 +header {* Simple example for table-based implementation of the reflexive transitive closure *}
     3.7 +
     3.8 +theory Transitive_Closure_Table_Ex
     3.9 +imports "~~/src/HOL/Library/Transitive_Closure_Table"
    3.10 +begin
    3.11 +
    3.12 +datatype ty = A | B | C
    3.13 +
    3.14 +inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
    3.15 +where
    3.16 +  "test A B"
    3.17 +| "test B A"
    3.18 +| "test B C"
    3.19 +
    3.20 +
    3.21 +text {* Invoking with the predicate compiler and the generic code generator *}
    3.22 +
    3.23 +code_pred test .
    3.24 +
    3.25 +values "{x. test\<^sup>*\<^sup>* A C}"
    3.26 +values "{x. test\<^sup>*\<^sup>* C A}"
    3.27 +values "{x. test\<^sup>*\<^sup>* A x}"
    3.28 +values "{x. test\<^sup>*\<^sup>* x C}"
    3.29 +
    3.30 +value "test\<^sup>*\<^sup>* A C"
    3.31 +value "test\<^sup>*\<^sup>* C A"
    3.32 +
    3.33 +end