*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] looking for some measure.union_inter theorem*From*: Henri DEBRAT <Henri.Debrat at loria.fr>*Date*: Tue, 6 Nov 2012 00:49:07 +0100*In-reply-to*: <31EA8FC5-7117-46B7-A2DA-2427F83AF044@loria.fr>*References*: <31EA8FC5-7117-46B7-A2DA-2427F83AF044@loria.fr>

> > I feel a little lost from this point, as I do not understand why f(A) + 0 = f(A) for any peculiar function f ! As far a I know, this is part of the addition definition. I meant "I do not understand why f(A) + 0 = f(A) SHOULD BE PROVED for any peculiar function f ", of course...

**References**:**[isabelle] looking for some measure.union_inter theorem***From:*Henri DEBRAT

- Previous by Date: [isabelle] looking for some measure.union_inter theorem
- Next by Date: Re: [isabelle] Isabelle operator precedence
- Previous by Thread: [isabelle] looking for some measure.union_inter theorem
- Next by Thread: Re: [isabelle] looking for some measure.union_inter theorem
- Cl-isabelle-users November 2012 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