*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] syntax translation*From*: li yongjian <lyj238 at gmail.com>*Date*: Thu, 29 Nov 2012 13:39:38 +0800

Dear expert: I want to define a syntax abbreaviation as follows: In latex source $n1\rightarrow_{SP}n2 \equiv (n1,n2) \in casual SP$ (please see the figures in attachment), where casual1 is defined as follows: definition casual1:: "strand_space \<Rightarrow>( node \<times> node ) set " where "casual1 SP \<equiv> { (n1,n2) . n1 \<in> Domain SP \<and> n2 \<in> Domain SP \<and> node_sign SP n1= + \<and> node_sign SP n2= - \<and> node_term SP n1= node_term SP n2 \<and> strand n1 \<noteq> strand n2 } " I have tried the following code, however, it cannot pass, can you give me a hand? syntax "_casual1"::" [node,strand_space,node]\<Rightarrow>bool" ( "_\<rightarrow>_/ _" ) translations "n1\<rightarrow>SP n2" == "CONST member (n1,n2) (casual1 SP)" regards lyj

**Attachment:
syntax.png**

**Follow-Ups**:**Re: [isabelle] syntax translation***From:*Tobias Nipkow

- Previous by Date: [isabelle] Basic IsarToLatex markup completed
- Next by Date: Re: [isabelle] syntax translation
- Previous by Thread: Re: [isabelle] Basic IsarToLatex markup completed
- Next by Thread: Re: [isabelle] syntax translation
- Cl-isabelle-users November 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