# HG changeset patch # User traytel # Date 1416420734 -3600 # Node ID be4a911aca712cc928d1f798488205ce7c5fac92 # Parent 627a93f6718295e365040ae37ebecdc8c9591371 more accurate lemma name diff -r 627a93f67182 -r be4a911aca71 src/HOL/Library/Stream.thy --- a/src/HOL/Library/Stream.thy Wed Nov 19 10:31:15 2014 +0100 +++ b/src/HOL/Library/Stream.thy Wed Nov 19 19:12:14 2014 +0100 @@ -380,7 +380,7 @@ qed qed simp -lemma same_cycle: "sconst x = cycle [x]" +lemma sconst_cycle: "sconst x = cycle [x]" by coinduction auto lemma smap_sconst: "smap f (sconst x) = sconst (f x)"