author | wenzelm |
Mon, 07 Nov 2005 19:03:02 +0100 | |
changeset 18109 | 94b528311e22 |
parent 18108 | 1e4516e68a58 |
child 18110 | 08ec4f1f116d |
--- a/src/HOLCF/ex/Stream.thy Mon Nov 07 18:50:53 2005 +0100 +++ b/src/HOLCF/ex/Stream.thy Mon Nov 07 19:03:02 2005 +0100 @@ -71,7 +71,7 @@ lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU & x = a && y)" by (auto,insert stream.exhaust [of x],auto) -lemma stream_neq_UU: "x~=UU ==> EX a as. x=a&&as & a~=UU" +lemma stream_neq_UU: "x~=UU ==> EX a a_s. x=a&&a_s & a~=UU" by (simp add: stream_exhaust_eq,auto) lemma stream_inject_eq [simp]: