--- a/src/HOL/Transitive_Closure.ML Tue Dec 05 22:14:53 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-
-(* 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";