From 43223f0fd8c99a6f85fbcf206e34aef7b8ffe47c Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 23 Dec 2003 12:24:06 +0000 Subject: removed bold, no longer supported by x-symbol --- isa/Example-Xsym.ML | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'isa/Example-Xsym.ML') diff --git a/isa/Example-Xsym.ML b/isa/Example-Xsym.ML index c9d40747..ed97c291 100644 --- a/isa/Example-Xsym.ML +++ b/isa/Example-Xsym.ML @@ -5,7 +5,7 @@ Just a version of Example.ML using XSymbol. - Also subscripts/superscripts/bold: A\<^sup>1 \\ A\<^sub>2 \\ A\<^bold>3 + Also subscripts/superscripts: A\<^sup>1 \\ A\<^sub>2 [NB: these can't be used in identifiers or otherwise parsed by Isabelle unless declared as part of a theory's concrete syntax, see docs or examples in HOL/IMP.] -- cgit v1.2.3