Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Transitive_Closure.ML
author wenzelm
Fri, 21 May 2004 21:26:19 +0200
changeset 14790 0d984ee030a1
parent 13704 854501b1e957
permissions -rw-r--r--
major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12691
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset 
     1
 












d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




     2


(* legacy ML bindings *)













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




     3














d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




     4


val converse_rtranclE = thm "converse_rtranclE";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




     5


val converse_rtranclE2 = thm "converse_rtranclE2";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




     6


val converse_rtrancl_induct = thm "converse_rtrancl_induct";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




     7


val converse_rtrancl_induct2 = thm "converse_rtrancl_induct2";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




     8


val converse_rtrancl_into_rtrancl = thm "converse_rtrancl_into_rtrancl";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




     9


val converse_trancl_induct = thm "converse_trancl_induct";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    10


val irrefl_tranclI = thm "irrefl_tranclI";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    11


val irrefl_trancl_rD = thm "irrefl_trancl_rD";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    12


val r_comp_rtrancl_eq = thm "r_comp_rtrancl_eq";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    13


val r_into_rtrancl = thm "r_into_rtrancl";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    14


val r_into_trancl = thm "r_into_trancl";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    15


val rtranclE = thm "rtranclE";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    16


val rtrancl_Un_rtrancl = thm "rtrancl_Un_rtrancl";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    17


val rtrancl_converse = thm "rtrancl_converse";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    18


val rtrancl_converseD = thm "rtrancl_converseD";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    19


val rtrancl_converseI = thm "rtrancl_converseI";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    20


val rtrancl_idemp = thm "rtrancl_idemp";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    21


val rtrancl_idemp_self_comp = thm "rtrancl_idemp_self_comp";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    22


val rtrancl_induct = thm "rtrancl_induct";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    23


val rtrancl_induct2 = thm "rtrancl_induct2";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    24


val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    25


val rtrancl_into_trancl1 = thm "rtrancl_into_trancl1";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    26


val rtrancl_into_trancl2 = thm "rtrancl_into_trancl2";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    27


val rtrancl_mono = thm "rtrancl_mono";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    28


val rtrancl_r_diff_Id = thm "rtrancl_r_diff_Id";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    29


val rtrancl_refl = thm "rtrancl_refl";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    30


val rtrancl_reflcl = thm "rtrancl_reflcl";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    31


val rtrancl_subset = thm "rtrancl_subset";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    32


val rtrancl_subset_rtrancl = thm "rtrancl_subset_rtrancl";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    33


val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    34


val rtrancl_trans = thm "rtrancl_trans";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    35


val tranclD = thm "tranclD";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    36


val tranclE = thm "tranclE";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    37


val trancl_converse = thm "trancl_converse";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    38


val trancl_converseD = thm "trancl_converseD";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    39


val trancl_converseI = thm "trancl_converseI";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    40


val trancl_induct = thm "trancl_induct";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    41


val trancl_insert = thm "trancl_insert";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    42


val trancl_into_rtrancl = thm "trancl_into_rtrancl";








13704






854501b1e957
Transitive closure is now defined inductively as well.



berghofe


parents: 
12691

diff
changeset




    43


val trancl_into_trancl = thm "trancl_into_trancl";








12691






d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    44


val trancl_into_trancl2 = thm "trancl_into_trancl2";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    45


val trancl_mono = thm "trancl_mono";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    46


val trancl_subset_Sigma = thm "trancl_subset_Sigma";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    47


val trancl_trans = thm "trancl_trans";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    48


val trancl_trans_induct = thm "trancl_trans_induct";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    49


val trans_rtrancl = thm "trans_rtrancl";













d21db58bcdc2
converted theory Transitive_Closure;



wenzelm


parents: 

diff
changeset




    50


val trans_trancl = thm "trans_trancl";















isabelle