diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-12-01 10:06:49 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-12-01 10:06:49 +0000 |
| commit | db4f7b2d60c42a432b8a0a97f796ab48460b4fb0 (patch) | |
| tree | 72ec02a1a2b575a3166e58dbd2ff321fce07f72a /etc/isar | |
| parent | ba2f03865ef50975d5ac2b0261d93fbe4b4eb837 (diff) | |
Add some examples of longer subscripts
Diffstat (limited to 'etc/isar')
| -rw-r--r-- | etc/isar/TokensAcid.thy | 15 |
1 files changed, 8 insertions, 7 deletions
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]\<Rightarrow>'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>\<gamma>\<delta>" (* 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 \<And> 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. |