equal
deleted
inserted
replaced
166 term fold1 |
166 term fold1 |
167 term fold |
167 term fold |
168 thm fold_def |
168 thm fold_def |
169 |
169 |
170 local_setup {* |
170 local_setup {* |
171 make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
171 make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn |
|
172 @{typ "'a list"} @{typ "'a fset"} #> snd |
172 *} |
173 *} |
173 |
174 |
174 term map |
175 term map |
175 term fmap |
176 term fmap |
176 thm fmap_def |
177 thm fmap_def |
|
178 |
|
179 |
177 |
180 |
178 |
181 |
179 ML {* |
182 ML {* |
180 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
183 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
181 @{const_name "membship"}, @{const_name "card1"}, |
184 @{const_name "membship"}, @{const_name "card1"}, |