author | traytel |
Wed, 19 Nov 2014 19:12:14 +0100 | |
changeset 59016 | be4a911aca71 |
parent 59015 | 627a93f67182 |
child 59017 | 80290f06a810 |
--- 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)"