*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] eta-contracted definitions and unfolding*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 08 Apr 2009 11:00:50 -0700*In-reply-to*: <alpine.LNX.1.10.0904081214010.31219@atbroy100.informatik.tu-muenchen.de>*References*: <1885A68F-9E4C-490E-A983-37F8E7A195E9@gmail.com> <alpine.LNX.1.10.0904081214010.31219@atbroy100.informatik.tu-muenchen.de>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

Quoting Makarius <makarius at sketis.net>:

On Wed, 8 Apr 2009, Peter Gammie wrote:definition "f' x y ≡ x + y" definition "g' x y ≡ y + x" lemma "f' = g'" unfolding f_def g_def sorryFor now you can use the following workaround: lemma "f' = g'" unfolding f_def_raw g_def_raw ...

definition "f' x y = x + y" definition "g' x y = y + x" lemma foo: "(%x y. f' x y) = (%x y. g' x y)" unfolding f'_def g'_def sorry

lemma bar: "f' = g'" by (rule foo) - Brian

**References**:**[isabelle] eta-contracted definitions and unfolding***From:*Peter Gammie

**Re: [isabelle] eta-contracted definitions and unfolding***From:*Makarius

- Previous by Date: [isabelle] ICFEM 2009: First Call for Papers
- Next by Date: [isabelle] Final CFP: Special Issue of the Journal of Automated Reasoning on Computer Security: Foundations and Automated Reasoning
- Previous by Thread: Re: [isabelle] eta-contracted definitions and unfolding
- Next by Thread: Re: [isabelle] eta-contracted definitions and unfolding
- Cl-isabelle-users April 2009 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