Re: [isabelle] Isabelle 2005



On Saturday 15 October 2005 21:36, John Ridgway wrote:
> Am I correct in believing that the definition of o_m in the Map library has
> changed?  The new definition is clearly map composition, whereas I believe
> that it used to be (June, 2005 versions of Isabelle) the image of a map
> under a function.  Is this correct?
Yes.

> Is there now any standard image of a 
> map under a function or do I need to add my own?
There is no operator defined. You have to add your own or write:

option_map f  o  m


   Norbert





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.