src/HOL/Transitive_Closure.ML
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 13704 854501b1e957
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 
     2 (* legacy ML bindings *)
     3 
     4 val converse_rtranclE = thm "converse_rtranclE";
     5 val converse_rtranclE2 = thm "converse_rtranclE2";
     6 val converse_rtrancl_induct = thm "converse_rtrancl_induct";
     7 val converse_rtrancl_induct2 = thm "converse_rtrancl_induct2";
     8 val converse_rtrancl_into_rtrancl = thm "converse_rtrancl_into_rtrancl";
     9 val converse_trancl_induct = thm "converse_trancl_induct";
    10 val irrefl_tranclI = thm "irrefl_tranclI";
    11 val irrefl_trancl_rD = thm "irrefl_trancl_rD";
    12 val r_comp_rtrancl_eq = thm "r_comp_rtrancl_eq";
    13 val r_into_rtrancl = thm "r_into_rtrancl";
    14 val r_into_trancl = thm "r_into_trancl";
    15 val rtranclE = thm "rtranclE";
    16 val rtrancl_Un_rtrancl = thm "rtrancl_Un_rtrancl";
    17 val rtrancl_converse = thm "rtrancl_converse";
    18 val rtrancl_converseD = thm "rtrancl_converseD";
    19 val rtrancl_converseI = thm "rtrancl_converseI";
    20 val rtrancl_idemp = thm "rtrancl_idemp";
    21 val rtrancl_idemp_self_comp = thm "rtrancl_idemp_self_comp";
    22 val rtrancl_induct = thm "rtrancl_induct";
    23 val rtrancl_induct2 = thm "rtrancl_induct2";
    24 val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl";
    25 val rtrancl_into_trancl1 = thm "rtrancl_into_trancl1";
    26 val rtrancl_into_trancl2 = thm "rtrancl_into_trancl2";
    27 val rtrancl_mono = thm "rtrancl_mono";
    28 val rtrancl_r_diff_Id = thm "rtrancl_r_diff_Id";
    29 val rtrancl_refl = thm "rtrancl_refl";
    30 val rtrancl_reflcl = thm "rtrancl_reflcl";
    31 val rtrancl_subset = thm "rtrancl_subset";
    32 val rtrancl_subset_rtrancl = thm "rtrancl_subset_rtrancl";
    33 val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
    34 val rtrancl_trans = thm "rtrancl_trans";
    35 val tranclD = thm "tranclD";
    36 val tranclE = thm "tranclE";
    37 val trancl_converse = thm "trancl_converse";
    38 val trancl_converseD = thm "trancl_converseD";
    39 val trancl_converseI = thm "trancl_converseI";
    40 val trancl_induct = thm "trancl_induct";
    41 val trancl_insert = thm "trancl_insert";
    42 val trancl_into_rtrancl = thm "trancl_into_rtrancl";
    43 val trancl_into_trancl = thm "trancl_into_trancl";
    44 val trancl_into_trancl2 = thm "trancl_into_trancl2";
    45 val trancl_mono = thm "trancl_mono";
    46 val trancl_subset_Sigma = thm "trancl_subset_Sigma";
    47 val trancl_trans = thm "trancl_trans";
    48 val trancl_trans_induct = thm "trancl_trans_induct";
    49 val trans_rtrancl = thm "trans_rtrancl";
    50 val trans_trancl = thm "trans_trancl";