From 6b7b2174bf06e9b2d2179001d83a8b1a453a5576 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 1 Dec 2009 10:27:49 +0000 Subject: Added spanning identifier supers/subs --- etc/isar/TokensAcid.thy | 8 ++++++-- 1 file 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>\\" (* 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, -- cgit v1.2.3