*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] equality of functions*From*: Roger H. <s57076 at hotmail.com>*Date*: Fri, 10 Jan 2014 17:54:12 +0200*Importance*: Normal

Hi, 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? Thank you!

**Follow-Ups**:**Re: [isabelle] equality of functions***From:*IG BI

**Re: [isabelle] equality of functions***From:*Manuel Eberl

**Re: [isabelle] equality of functions***From:*IG BI

- Previous by Date: Re: [isabelle] Add a definition to the simplifier
- Next by Date: Re: [isabelle] equality of functions
- Previous by Thread: [isabelle] Isabelle 2013 / Print goals on failed proof method
- Next by Thread: Re: [isabelle] equality of functions
- 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