avoid 'as' as identifier;
authorwenzelm
Mon, 07 Nov 2005 19:03:02 +0100
changeset 18109 94b528311e22
parent 18108 1e4516e68a58
child 18110 08ec4f1f116d
avoid 'as' as identifier;
src/HOLCF/ex/Stream.thy
--- 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]: