# HG changeset patch # User huffman # Date 1240266207 25200 # Node ID ceeb5f2eac757e99ad2dbdda901f54e0cbc104a9 # Parent 10b26965a08f984a1b0852784c78424e70214d28 fix too-specific types in lemmas match_{sinl,sinr}_simps diff -r 10b26965a08f -r ceeb5f2eac75 src/HOLCF/Fixrec.thy --- a/src/HOLCF/Fixrec.thy Mon Apr 13 09:29:55 2009 -0700 +++ b/src/HOLCF/Fixrec.thy Mon Apr 20 15:23:27 2009 -0700 @@ -534,13 +534,13 @@ lemma match_sinl_simps [simp]: "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x)\<cdot>k = k\<cdot>x" - "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x)\<cdot>k = fail" + "y \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>y)\<cdot>k = fail" "match_sinl\<cdot>\<bottom>\<cdot>k = \<bottom>" by (simp_all add: match_sinl_def) lemma match_sinr_simps [simp]: - "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x)\<cdot>k = k\<cdot>x" "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x)\<cdot>k = fail" + "y \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>y)\<cdot>k = k\<cdot>y" "match_sinr\<cdot>\<bottom>\<cdot>k = \<bottom>" by (simp_all add: match_sinr_def)