From 5301fd94b22fa5e59dfcccc19e89e2f3faccd21e Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 26 Aug 2002 14:12:48 +0000
Subject: Add example of sub/sup/bold in comment.

---
 isa/Example-Xsym.ML | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'isa/Example-Xsym.ML')

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";
-- 
cgit v1.2.3