--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy Wed Dec 30 21:23:38 2015 +0100
@@ -44,11 +44,11 @@
"<> == \<bottom>"
abbreviation
- fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63) where
- "A(C)s == fsfilter A\<cdot>s"
+ fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<copyright>_)" [64,63] 63) where
+ "A\<copyright>s == fsfilter A\<cdot>s"
-notation (xsymbols)
- fsfilter' ("(_\<copyright>_)" [64,63] 63)
+notation (ASCII)
+ fsfilter' ("(_'(C')_)" [64,63] 63)
lemma ft_fsingleton[simp]: "ft$(<a>) = Def a"