equal
deleted
inserted
replaced
167 term fold |
167 term fold |
168 thm fold_def |
168 thm fold_def |
169 |
169 |
170 (* FIXME: does not work yet for all types*) |
170 (* FIXME: does not work yet for all types*) |
171 quotient_def (for "'a fset") |
171 quotient_def (for "'a fset") |
172 fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
172 fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
173 where |
173 where |
174 "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)" |
174 "fmap \<equiv> (map::('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list)" |
175 |
175 |
176 term map |
176 term map |
177 term fmap |
177 term fmap |
178 thm fmap_def |
178 thm fmap_def |
179 |
179 |