*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] equality of functions*From*: IG BI <igbi at gmx.com>*Date*: Fri, 10 Jan 2014 11:40:27 -0600*In-reply-to*: <DUB124-W437699E714D19647864BCD8FB30@phx.gbl>*References*: <DUB124-W437699E714D19647864BCD8FB30@phx.gbl>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 1/10/2014 9:54 AM, Roger H. wrote:

the lemma "[1 ↦ [4], 2 ↦ [5]] = [2 ↦ [5], 1 ↦ [4]]" can be proven by auto, but is there any automatic proof, meaning some existing lemma, which i can add to the simplifier, so that such identities that occur in the middle of proofs are solved automatically?

Regards, GB

**References**:**[isabelle] equality of functions***From:*Roger H .

- Previous by Date: Re: [isabelle] equality of functions
- Next by Date: Re: [isabelle] Build HOL
- Previous by Thread: Re: [isabelle] equality of functions
- Next by Thread: [isabelle] AFP: first entry for 2014
- 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