# HG changeset patch
# User huffman
# Date 1287665078 25200
# Node ID 748911a00a5141a6a7a51347c84e60190679d764
# Parent  435f9f5970f813ad7df83a2437dfbfc740e6d53a
remove intro! attribute from {sinl,sinr}_defined

diff -r 435f9f5970f8 -r 748911a00a51 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Thu Oct 21 05:35:32 2010 -0700
+++ b/src/HOLCF/Ssum.thy	Thu Oct 21 05:44:38 2010 -0700
@@ -108,10 +108,10 @@
 lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
 using sinr_eq [of "x" "\<bottom>"] by simp
 
-lemma sinl_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
+lemma sinl_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
 by simp
 
-lemma sinr_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
+lemma sinr_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
 by simp
 
 text {* Compactness *}