# 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\x = \) = (x = \)" using sinr_eq [of "x" "\"] by simp -lemma sinl_defined [intro!]: "x \ \ \ sinl\x \ \" +lemma sinl_defined: "x \ \ \ sinl\x \ \" by simp -lemma sinr_defined [intro!]: "x \ \ \ sinr\x \ \" +lemma sinr_defined: "x \ \ \ sinr\x \ \" by simp text {* Compactness *}