src/HOL/Library/Stream.thy

 theory Stream
   imports Nat_Bijection
 begin
 
 codatatype (sset: 'a) stream =
-  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
+  SCons (shd: 'a) (stl: "'a stream") (infixr \<open>##\<close> 65)
 for
   map: smap
   rel: stream_all2
 
 context

 lemma smap_ctr: "smap f s = x ## s' \<longleftrightarrow> f (shd s) = x \<and> smap f (stl s) = s'"
   by (cases s) simp
 
 subsection \<open>prepend list to stream\<close>
 
-primrec shift :: "'a list \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr "@-" 65) where
+primrec shift :: "'a list \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr \<open>@-\<close> 65) where
   "shift [] s = s"
 | "shift (x # xs) s = x ## shift xs s"
 
 lemma smap_shift[simp]: "smap f (xs @- s) = map f xs @- smap f s"
   by (induct xs) auto

 lemma streams_UNIV[simp]: "streams UNIV = UNIV"
   by (auto simp: streams_iff_sset)
 
 subsection \<open>nth, take, drop for streams\<close>
 
-primrec snth :: "'a stream \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
+primrec snth :: "'a stream \<Rightarrow> nat \<Rightarrow> 'a" (infixl \<open>!!\<close> 100) where
   "s !! 0 = shd s"
 | "s !! Suc n = stl s !! n"
 
 lemma snth_Stream: "(x ## s) !! Suc i = s !! i"
   by simp