(* legacy ML bindings *) val converse_rtranclE = thm "converse_rtranclE"; val converse_rtranclE2 = thm "converse_rtranclE2"; val converse_rtrancl_induct = thm "converse_rtrancl_induct"; val converse_rtrancl_induct2 = thm "converse_rtrancl_induct2"; val converse_rtrancl_into_rtrancl = thm "converse_rtrancl_into_rtrancl"; val converse_trancl_induct = thm "converse_trancl_induct"; val irrefl_tranclI = thm "irrefl_tranclI"; val irrefl_trancl_rD = thm "irrefl_trancl_rD"; val r_comp_rtrancl_eq = thm "r_comp_rtrancl_eq"; val r_into_rtrancl = thm "r_into_rtrancl"; val r_into_trancl = thm "r_into_trancl"; val rtranclE = thm "rtranclE"; val rtrancl_Un_rtrancl = thm "rtrancl_Un_rtrancl"; val rtrancl_converse = thm "rtrancl_converse"; val rtrancl_converseD = thm "rtrancl_converseD"; val rtrancl_converseI = thm "rtrancl_converseI"; val rtrancl_idemp = thm "rtrancl_idemp"; val rtrancl_idemp_self_comp = thm "rtrancl_idemp_self_comp"; val rtrancl_induct = thm "rtrancl_induct"; val rtrancl_induct2 = thm "rtrancl_induct2"; val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl"; val rtrancl_into_trancl1 = thm "rtrancl_into_trancl1"; val rtrancl_into_trancl2 = thm "rtrancl_into_trancl2"; val rtrancl_mono = thm "rtrancl_mono"; val rtrancl_r_diff_Id = thm "rtrancl_r_diff_Id"; val rtrancl_refl = thm "rtrancl_refl"; val rtrancl_reflcl = thm "rtrancl_reflcl"; val rtrancl_subset = thm "rtrancl_subset"; val rtrancl_subset_rtrancl = thm "rtrancl_subset_rtrancl"; val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl"; val rtrancl_trans = thm "rtrancl_trans"; val tranclD = thm "tranclD"; val tranclE = thm "tranclE"; val trancl_converse = thm "trancl_converse"; val trancl_converseD = thm "trancl_converseD"; val trancl_converseI = thm "trancl_converseI"; val trancl_induct = thm "trancl_induct"; val trancl_insert = thm "trancl_insert"; val trancl_into_rtrancl = thm "trancl_into_rtrancl"; val trancl_into_trancl = thm "trancl_into_trancl"; val trancl_into_trancl2 = thm "trancl_into_trancl2"; val trancl_mono = thm "trancl_mono"; val trancl_subset_Sigma = thm "trancl_subset_Sigma"; val trancl_trans = thm "trancl_trans"; val trancl_trans_induct = thm "trancl_trans_induct"; val trans_rtrancl = thm "trans_rtrancl"; val trans_trancl = thm "trans_trancl";