diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-12-01 10:27:49 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-12-01 10:27:49 +0000 |
| commit | 6b7b2174bf06e9b2d2179001d83a8b1a453a5576 (patch) | |
| tree | a37254220b9e16f9e9c5efc8b079a95558a48bf4 /etc/isar/TokensAcid.thy | |
| parent | db570710763e4209ee7e0b093e6bbb73ca48cb2f (diff) | |
Added spanning identifier supers/subs
Diffstat (limited to 'etc/isar/TokensAcid.thy')
| -rw-r--r-- | etc/isar/TokensAcid.thy | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/etc/isar/TokensAcid.thy b/etc/isar/TokensAcid.thy index 744bdb54..f3773497 100644 --- a/etc/isar/TokensAcid.thy +++ b/etc/isar/TokensAcid.thy @@ -119,14 +119,18 @@ term "\<^loc>a" term "\<^bold>b" term "\<^italic>b" -(* More taxing examples *) +(* Further examples *) term "a\<^isub>\<gamma>\<delta>" (* subscripted gamma *) -term "a\<^isub>def" (* no subscript on bc *) +term "a\<^isub>def" (* no subscript on ef *) 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 *) +(* Spanning identifier supers/subs: to be added to Isabelle lexer/latex *) + +term "a\<^bisup>bcd\<^eisup>" +term "a\<^bisub>bcd\<^eisub>" (* Variants on token names: different token names, |