| changeset 16752 | 270ec60cc9e8 |
| parent 16699 | 24b494ff8f0f |
| child 16922 | 2128ac2aa5db |
--- a/src/HOLCF/Ssum.ML Fri Jul 08 02:38:05 2005 +0200 +++ b/src/HOLCF/Ssum.ML Fri Jul 08 02:39:53 2005 +0200 @@ -14,7 +14,6 @@ val cont_Iwhen3 = thm "cont_Iwhen3"; val sinl_strict = thm "sinl_strict"; val sinr_strict = thm "sinr_strict"; -val noteq_sinlsinr = thm "noteq_sinlsinr"; val sinl_inject = thm "sinl_inject"; val sinr_inject = thm "sinr_inject"; val sinl_eq = thm "sinl_eq";