equal
deleted
inserted
replaced
42 abbreviation |
42 abbreviation |
43 emptystream :: "'a fstream" ("<>") where |
43 emptystream :: "'a fstream" ("<>") where |
44 "<> == \<bottom>" |
44 "<> == \<bottom>" |
45 |
45 |
46 abbreviation |
46 abbreviation |
47 fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63) where |
47 fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<copyright>_)" [64,63] 63) where |
48 "A(C)s == fsfilter A\<cdot>s" |
48 "A\<copyright>s == fsfilter A\<cdot>s" |
49 |
49 |
50 notation (xsymbols) |
50 notation (ASCII) |
51 fsfilter' ("(_\<copyright>_)" [64,63] 63) |
51 fsfilter' ("(_'(C')_)" [64,63] 63) |
52 |
52 |
53 |
53 |
54 lemma ft_fsingleton[simp]: "ft$(<a>) = Def a" |
54 lemma ft_fsingleton[simp]: "ft$(<a>) = Def a" |
55 by (simp add: fsingleton_def2) |
55 by (simp add: fsingleton_def2) |
56 |
56 |