--- a/src/HOLCF/Ssum.ML Fri Mar 11 23:58:31 2005 +0100
+++ b/src/HOLCF/Ssum.ML Sat Mar 12 00:07:05 2005 +0100
@@ -4,19 +4,9 @@
val Isinl_def = thm "Isinl_def";
val Isinr_def = thm "Isinr_def";
val Iwhen_def = thm "Iwhen_def";
-val SsumIl = thm "SsumIl";
-val SsumIr = thm "SsumIr";
val inj_on_Abs_Ssum = thm "inj_on_Abs_Ssum";
-val strict_SinlSinr_Rep = thm "strict_SinlSinr_Rep";
val strict_IsinlIsinr = thm "strict_IsinlIsinr";
-val noteq_SinlSinr_Rep = thm "noteq_SinlSinr_Rep";
val noteq_IsinlIsinr = thm "noteq_IsinlIsinr";
-val inject_Sinl_Rep1 = thm "inject_Sinl_Rep1";
-val inject_Sinr_Rep1 = thm "inject_Sinr_Rep1";
-val inject_Sinl_Rep2 = thm "inject_Sinl_Rep2";
-val inject_Sinr_Rep2 = thm "inject_Sinr_Rep2";
-val inject_Sinl_Rep = thm "inject_Sinl_Rep";
-val inject_Sinr_Rep = thm "inject_Sinr_Rep";
val inject_Isinl = thm "inject_Isinl";
val inject_Isinr = thm "inject_Isinr";
val inject_Isinl_rev = thm "inject_Isinl_rev";