*To*: Peter Sewell <Peter.Sewell at cl.cam.ac.uk>*Subject*: Re: [isabelle] typesetting compound subscripts*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Thu, 14 Feb 2008 16:55:41 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <E1JNoeb-0007u7-00@mta2.cl.cam.ac.uk>*Organization*: Technische Universität München*References*: <E1JNoeb-0007u7-00@mta2.cl.cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.13) Gecko/20060417

Peter Sewell wrote:

Dear Isabelle, How is it possible to introduce typeset syntax with compound subscripts? For example, given an indexed family "tos" of relations,where I currently write(t1,t2) \<in> tos nI'd like to write something that will be typeset roughly as the LaTeXt1 \leq_{tos n} t2 (Here tos is a bound variable, not something introduced by a consts, if that makes any difference.) My attempts have all failed miserably (except when the subscript is a single-character identifier), trying various combinations of Isabelle syntax and translations declarations, definitions of \isactrlfoo's, and \<^bsub>...\<^esub>.

Dear Peter, this could be achieved by introducing an abbreviation mapping x \<le>\<^bsub>R\<^esub> y to (x, y) \<in> R as shown in the attached theory file. Note that this abbreviation will affect all terms of the form "(x, y) \<in> R", which for example means that also the intoduction rules for the transitive closure are printed using this syntax. Greetings, Stefan -- Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de Institut fuer Informatik Phone: +49 89 289 17328 Technische Universitaet Muenchen Fax: +49 89 289 17307 Boltzmannstr. 3 Room: 01.11.059 85748 Garching, GERMANY http://www.in.tum.de/~berghofe

theory Peter imports Main begin types t = "string" types indexed_orders = "nat \<Rightarrow> (t*t) set" constdefs mytest :: "indexed_orders \<Rightarrow> nat \<Rightarrow> t \<Rightarrow> t \<Rightarrow> bool" "mytest tos n t1 t2 == (t1,t2) \<in> tos n" abbreviation in_rel :: "'a \<Rightarrow> ('a * 'b) set \<Rightarrow> 'b \<Rightarrow> bool" ("(_/ \<le>\<^bsub>_\<^esub> _)" [51, 0, 51] 50) where "x \<le>\<^bsub>R\<^esub> y \<equiv> (x, y) \<in> R" text {* The definition of @{text mytest} is @{thm [display] mytest_def [no_vars]} The introduction rule @{text rtrancl_into_rtrancl} for the transitive closure is @{thm [display] rtrancl_into_rtrancl [no_vars]} *} end

**Follow-Ups**:**Re: [isabelle] typesetting compound subscripts***From:*Peter Sewell

**References**:**[isabelle] typesetting compound subscripts***From:*Peter Sewell

- Previous by Date: Re: [isabelle] Syntax and inductive_set
- Next by Date: [isabelle] LFMTP'08 call for papers
- Previous by Thread: [isabelle] typesetting compound subscripts
- Next by Thread: Re: [isabelle] typesetting compound subscripts
- Cl-isabelle-users February 2008 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