From db4f7b2d60c42a432b8a0a97f796ab48460b4fb0 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 1 Dec 2009 10:06:49 +0000 Subject: Add some examples of longer subscripts --- etc/isar/TokensAcid.thy | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'etc/isar') diff --git a/etc/isar/TokensAcid.thy b/etc/isar/TokensAcid.thy index 408dfd73..744bdb54 100644 --- a/etc/isar/TokensAcid.thy +++ b/etc/isar/TokensAcid.thy @@ -115,16 +115,17 @@ consts charitalic :: "['a,'a]\'a" ("\<^italic>_") term "a\<^sub>b" term "a\<^sup>b" -term "a\<^isub>abc" -term "a\<^isup>abc" term "\<^loc>a" term "\<^bold>b" term "\<^italic>b" -(* More taxing examples for testing *) +(* More taxing examples *) -term "a\<^isub>x\<^isub>y" (* both x and y should be subscripted *) -term "a\<^isub>xabc\<^isub>y" (* both x.abc and y should be subscripted *) +term "a\<^isub>\\" (* subscripted gamma *) +term "a\<^isub>def" (* no subscript on bc *) + +term "a\<^isub>x\<^isub>y" (* x and y subscripted individually *) +term "a\<^isub>xabc\<^isub>y" (* x and y should be subscripted, but not ab *) (* @@ -136,8 +137,8 @@ term "a\<^isub>xabc\<^isub>y" (* both x.abc and y should be subscripted *) Demonstration: let's take back \ from the meta-level. NB: the token scheme mechanism here is a PG convenience, - in other frontends you may have to define \< AndX> to - appear in the same way as \< And> individually. + in other frontends you may have to define \ < AndX> to + appear in the same way as \ < And> individually. Similarly for LaTeX output. Use C-c C-t C-z to toggle the display of tokens. -- cgit v1.2.3