diff options
| -rw-r--r-- | isa/Example-Xsym.ML | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/isa/Example-Xsym.ML b/isa/Example-Xsym.ML index d566a850..c9d40747 100644 --- a/isa/Example-Xsym.ML +++ b/isa/Example-Xsym.ML @@ -3,7 +3,12 @@ $Id$ - Just a version of Example.ML using XSymbol + Just a version of Example.ML using XSymbol. + + Also subscripts/superscripts/bold: A\<^sup>1 \\<or> A\<^sub>2 \\<or> A\<^bold>3 + [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.] *) Goal "A \\<and> B \\<longrightarrow> B \\<and> A"; |