From 00f5da7faee18f460563785ebbb62dce10a70813 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 18 Aug 2010 15:58:06 +0000 Subject: Minor rearrange --- etc/isar/TokensAcid.thy | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'etc/isar') diff --git a/etc/isar/TokensAcid.thy b/etc/isar/TokensAcid.thy index 631ef336..30807b89 100644 --- a/etc/isar/TokensAcid.thy +++ b/etc/isar/TokensAcid.thy @@ -112,9 +112,6 @@ by auto See Tokens -> Format Char -> ... *) -(* NB: below here cannot be processed: just in terms to check with - string font for terms. *) - consts shortsub :: "['a,'a]\'a" ("_\<^sub>_") consts shortsup :: "['a,'a]\'a" ("_\<^sup>_") @@ -136,11 +133,6 @@ 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, same appearance. Simulated overloading, \<^bitalic>much\<^eitalic> simpler to do @@ -173,12 +165,21 @@ term "\ {\ x. True, \ y. False}" +(* NB: below here cannot be processed: just in terms to check with + string font for terms. *) + + +(* Spanning identifier supers/subs: to be added to Isabelle lexer/latex *) + +term "a\<^bisup>bcd\<^eisup>" +term "a\<^bisub>bcd\<^eisub>" + (* More esoteric stuff *) term "\<^bbig>large text \ \ \\<^ebig>" -term "\<^bsmall>small\<^esmall>" +term "\<^bsmall>small text \ \ \ \ \ \<^esmall>" term "\<^bunderline>underlined\<^eunderline>" -- cgit v1.2.3