equal
deleted
inserted
replaced
31 "a~>s == fscons a\<cdot>s" |
31 "a~>s == fscons a\<cdot>s" |
32 |
32 |
33 fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63) |
33 fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63) |
34 "A(C)s == fsfilter A\<cdot>s" |
34 "A(C)s == fsfilter A\<cdot>s" |
35 |
35 |
36 const_syntax (xsymbols) |
36 notation (xsymbols) |
37 fscons' ("(_\<leadsto>_)" [66,65] 65) |
37 fscons' ("(_\<leadsto>_)" [66,65] 65) |
38 fsfilter' ("(_\<copyright>_)" [64,63] 63) |
38 fsfilter' ("(_\<copyright>_)" [64,63] 63) |
39 |
39 |
40 |
40 |
41 lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d" |
41 lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d" |