src/HOL/Transitive_Closure.ML
changeset 12691 d21db58bcdc2
child 13704 854501b1e957
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Transitive_Closure.ML	Wed Jan 09 17:48:40 2002 +0100
     1.3 @@ -0,0 +1,50 @@
     1.4 +
     1.5 +(* legacy ML bindings *)
     1.6 +
     1.7 +val converse_rtranclE = thm "converse_rtranclE";
     1.8 +val converse_rtranclE2 = thm "converse_rtranclE2";
     1.9 +val converse_rtrancl_induct = thm "converse_rtrancl_induct";
    1.10 +val converse_rtrancl_induct2 = thm "converse_rtrancl_induct2";
    1.11 +val converse_rtrancl_into_rtrancl = thm "converse_rtrancl_into_rtrancl";
    1.12 +val converse_trancl_induct = thm "converse_trancl_induct";
    1.13 +val irrefl_tranclI = thm "irrefl_tranclI";
    1.14 +val irrefl_trancl_rD = thm "irrefl_trancl_rD";
    1.15 +val r_comp_rtrancl_eq = thm "r_comp_rtrancl_eq";
    1.16 +val r_into_rtrancl = thm "r_into_rtrancl";
    1.17 +val r_into_trancl = thm "r_into_trancl";
    1.18 +val rtranclE = thm "rtranclE";
    1.19 +val rtrancl_Un_rtrancl = thm "rtrancl_Un_rtrancl";
    1.20 +val rtrancl_converse = thm "rtrancl_converse";
    1.21 +val rtrancl_converseD = thm "rtrancl_converseD";
    1.22 +val rtrancl_converseI = thm "rtrancl_converseI";
    1.23 +val rtrancl_idemp = thm "rtrancl_idemp";
    1.24 +val rtrancl_idemp_self_comp = thm "rtrancl_idemp_self_comp";
    1.25 +val rtrancl_induct = thm "rtrancl_induct";
    1.26 +val rtrancl_induct2 = thm "rtrancl_induct2";
    1.27 +val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl";
    1.28 +val rtrancl_into_trancl1 = thm "rtrancl_into_trancl1";
    1.29 +val rtrancl_into_trancl2 = thm "rtrancl_into_trancl2";
    1.30 +val rtrancl_mono = thm "rtrancl_mono";
    1.31 +val rtrancl_r_diff_Id = thm "rtrancl_r_diff_Id";
    1.32 +val rtrancl_refl = thm "rtrancl_refl";
    1.33 +val rtrancl_reflcl = thm "rtrancl_reflcl";
    1.34 +val rtrancl_subset = thm "rtrancl_subset";
    1.35 +val rtrancl_subset_rtrancl = thm "rtrancl_subset_rtrancl";
    1.36 +val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
    1.37 +val rtrancl_trans = thm "rtrancl_trans";
    1.38 +val tranclD = thm "tranclD";
    1.39 +val tranclE = thm "tranclE";
    1.40 +val trancl_converse = thm "trancl_converse";
    1.41 +val trancl_converseD = thm "trancl_converseD";
    1.42 +val trancl_converseI = thm "trancl_converseI";
    1.43 +val trancl_def = thm "trancl_def";
    1.44 +val trancl_induct = thm "trancl_induct";
    1.45 +val trancl_insert = thm "trancl_insert";
    1.46 +val trancl_into_rtrancl = thm "trancl_into_rtrancl";
    1.47 +val trancl_into_trancl2 = thm "trancl_into_trancl2";
    1.48 +val trancl_mono = thm "trancl_mono";
    1.49 +val trancl_subset_Sigma = thm "trancl_subset_Sigma";
    1.50 +val trancl_trans = thm "trancl_trans";
    1.51 +val trancl_trans_induct = thm "trancl_trans_induct";
    1.52 +val trans_rtrancl = thm "trans_rtrancl";
    1.53 +val trans_trancl = thm "trans_trancl";