*To*: Stephan van Staden <Stephan.vanStaden at inf.ethz.ch>*Subject*: Re: [isabelle] Syntax, translations inside a locale*From*: Makarius <makarius at sketis.net>*Date*: Mon, 27 Feb 2012 14:49:10 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4F47B283.8000207@inf.ethz.ch>*References*: <4F47B283.8000207@inf.ethz.ch>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 24 Feb 2012, Stephan van Staden wrote:

I'm working in a locale where I have an associative and commutativeoperator + with unit 0. I want an alternative notation for it - anoperator, say {|_|}, with arbitrary (but finite) arity.Without Isabelle I would write: {| n1, n2, ..., nk |} =def n1 + n2 + ... + nkThen I want to prove/use theorems such as {|n1, n2|} + n3 = {|n1, n2, n3|},etc.In Isabelle, I've tried to write: syntax "MyNotation" :: "args => 'a" ("{|(_)|}") translations "{|x, xs|}" == "x + {|xs|}" "{| |}" == "0"However, it gives the error: 'Illegal application of command "syntax" inlocal theory mode'.Is there a simple way to do it properly in a locale?

Makarius

**References**:**[isabelle] Syntax, translations inside a locale***From:*Stephan van Staden

- Previous by Date: [isabelle] Call for Journal Papers: STVR Special Issue on Tests and Proofs
- Next by Date: [isabelle] THedu12 1st call for papers
- Previous by Thread: [isabelle] Syntax, translations inside a locale
- Next by Thread: [isabelle] ETAPS Workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012)
- Cl-isabelle-users February 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