*To*: Walther Neuper <wneuper at ist.tugraz.at>, <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] values from locales*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 7 Nov 2013 12:07:23 +0100*In-reply-to*: <527B6E77.6000204@ist.tugraz.at>*References*: <527B6E77.6000204@ist.tugraz.at>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.0

Hi Walter,

lemma [code]: "t a b = a + b"

Hope this helps, Andreas [1] http://www.infsec.ethz.ch/people/andreloc/publications/lochbihler11itp.pdf On 07/11/13 11:41, Walther Neuper wrote:

While studying ~~/doc/locales.pdf, ~~/doc/isar-ref.pdf and and code in Vector_Space.thy I got stuck with evaluating definitions occurring within locale: locale lll = fixes fff :: "int ⇒ int ⇒ int" assumes ccc: "fff a b = fff b a" begin lemma aaa [code]: "fff a b = a + b" sorry value "fff 1 2" --{*"fff 1 2" :: "int" --- EXPECT "3" HERE *} end Question: What am I missing in order to get value "fff 1 2" --{*"3" :: "int"*} Thanks for patience with this question, Walther PS: For pointers into ~~/doc I'd particularly grateful.

**Follow-Ups**:**Re: [isabelle] values from locales***From:*Walther Neuper

**References**:**[isabelle] values from locales***From:*Walther Neuper

- Previous by Date: [isabelle] values from locales
- Next by Date: Re: [isabelle] values from locales
- Previous by Thread: [isabelle] values from locales
- Next by Thread: Re: [isabelle] values from locales
- Cl-isabelle-users November 2013 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