equal
deleted
inserted
replaced
167 term fmap |
167 term fmap |
168 thm fmap_def |
168 thm fmap_def |
169 |
169 |
170 |
170 |
171 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} |
171 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} |
172 ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} |
172 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) |
173 |
173 |
174 (* ML {* |
174 ML {* |
175 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
175 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
176 @{const_name "membship"}, @{const_name "card1"}, |
176 @{const_name "membship"}, @{const_name "card1"}, |
177 @{const_name "append"}, @{const_name "fold1"}, |
177 @{const_name "append"}, @{const_name "fold1"}, |
178 @{const_name "map"}]; |
178 @{const_name "map"}]; |
179 *} *) |
179 *} |
180 |
180 |
181 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
181 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
182 |
182 |
183 lemma memb_rsp: |
183 lemma memb_rsp: |
184 fixes z |
184 fixes z |