| changeset 59016 | be4a911aca71 |
| parent 59000 | 6eb0725503fc |
| child 60011 | 3eef7a43cd51 |
--- 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)"