*To*: Andrew Boyton <Andrew.Boyton at nicta.com.au>*Subject*: Re: [isabelle] Partial functions basics*From*: Tjark Weber <webertj at in.tum.de>*Date*: Fri, 10 Jan 2014 05:26:06 +0100*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>, John Wickerson <johnwickerson at cantab.net>, "Roger H." <s57076 at hotmail.com>*In-reply-to*: <916DE6B1-1D54-4536-A619-5F5A35E2D1F6@nicta.com.au>*References*: <DUB124-W39CC062195AB276AD815958FB00@phx.gbl> <75BFEEB2-E851-4A3C-A2C8-0083058DDFE6@cantab.net> <916DE6B1-1D54-4536-A619-5F5A35E2D1F6@nicta.com.au>

On Thu, 2014-01-09 at 23:26 +0000, Andrew Boyton wrote: > Note that map_add does right overloading, and is thus not an > associative operator. Note that there is a theorem map_add_assoc that proves associativity of map_add. Perhaps you meant to write that map_add is not commutative. Best, Tjark

**References**:**[isabelle] Partial functions basics***From:*Roger H .

**Re: [isabelle] Partial functions basics***From:*John Wickerson

**Re: [isabelle] Partial functions basics***From:*Andrew Boyton

- Previous by Date: Re: [isabelle] Partial functions basics
- Next by Date: [isabelle] Build HOL
- Previous by Thread: Re: [isabelle] Partial functions basics
- Next by Thread: [isabelle] Build HOL
- Cl-isabelle-users January 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list