169   "fmap \<equiv> map"

   169   "fmap \<equiv> map"

   170 

   170 

   171 term map

   171 term map

   172 term fmap

   172 term fmap

   173 thm fmap_def

   173 thm fmap_def

   174 

   176 

   175 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}

   177 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}

   176 ML {* val consts = lookup_quot_consts defs *}

   178 ML {* val consts = lookup_quot_consts defs *}

   177 ML {* val defs_sym = add_lower_defs @{context} defs *}

   179 ML {* val defs_sym = add_lower_defs @{context} defs *}

   178 

   180