author | huffman |
Mon, 22 Mar 2010 23:33:02 -0700 | |
changeset 35924 | 384a31bd5425 |
parent 35923 | 9c59c490c4e5 |
child 35925 | 3da8db225c93 |
--- a/src/HOLCF/IOA/meta_theory/Seq.thy Mon Mar 22 23:02:43 2010 -0700 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy Mon Mar 22 23:33:02 2010 -0700 @@ -175,7 +175,7 @@ szip_nil: "szip$nil$y=nil" | szip_cons_nil: "x~=UU ==> szip$(x##xs)$nil=UU" | szip_cons: - "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##szip$xs$ys" + "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = (x,y)##szip$xs$ys" lemma szip_UU1 [simp]: "szip$UU$y=UU" by fixrec_simp