src/HOLCF/FOCUS/Stream_adm.thy

 
 constdefs
 
   stream_monoP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
   "stream_monoP F \<equiv> \<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow>
-                    (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i rt s \<in> P)"
+                    (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i\<cdot>rt\<cdot>s \<in> P)"
 
   stream_antiP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
   "stream_antiP F \<equiv> \<forall>P x. \<exists>Q i.
                 (#x  < Fin i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
                 (Fin i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
-                (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i rt y \<in> P)))"
+                (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P)))"
 
   antitonP :: "'a set => bool"
   "antitonP P \<equiv> \<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P"
 
 ML {* use_legacy_bindings (the_context ()) *}