# HG changeset patch
# User huffman
# Date 1110582425 -3600
# Node ID 30576c645e91e83428446a630756c0636c8ba4ba
# Parent  95617b30514b0c7a8ddf61c43583e5d91d7f0a1d
removed theorems about Sinl_Rep and Sinr_Rep

diff -r 95617b30514b -r 30576c645e91 src/HOLCF/Ssum.ML
--- 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";