From fc9e4ea7c47218b57664e2c20d04d2b4aae5dd81 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 10 Mar 2003 09:11:14 +0000
Subject: Add test case with symbol in subscript

---
 etc/isar/XSymbolTests.thy | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/etc/isar/XSymbolTests.thy b/etc/isar/XSymbolTests.thy
index 9095555c..09952ecd 100644
--- a/etc/isar/XSymbolTests.thy
+++ b/etc/isar/XSymbolTests.thy
@@ -37,9 +37,18 @@ consts
  "\<^bold>X"  :: bool   (* bold character *)
 
 
-(* Markus reports that \<cdot> is saved in the file as
- an 8-bit character.  I can't repeat that with XEmacs 21.4,
-unless I set the relevant X-Symbol menu option. *)
+(* test: using a symbol as a subscript *)
+(* 9.3.03: this causes nasty prob with pre-command hook,
+   x-symbol-invisitiblity-spec type error, at least
+   during editing. *)
+consts
+ intof :: nat \<Rightarrow> int  ("_\<^sub>\<int>" 50)
+ mynat :: nat ("\<gamma>")
+
+constdefs
+ myint :: int
+ "myint == \<gamma>\<^sub>\<int>"
+ 
 
 (* 
  Another X-Symbol oddity: sometimes the _first_ buffer to
-- 
cgit v1.2.3