diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-03-10 09:11:14 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-03-10 09:11:14 +0000 |
| commit | fc9e4ea7c47218b57664e2c20d04d2b4aae5dd81 (patch) | |
| tree | 92ebe4563b48317346b83d1991d66b97ffbeac54 /etc/isar | |
| parent | 27d1b93223310c8d55df6e85e3d4a9e9b354ab51 (diff) | |
Add test case with symbol in subscript
Diffstat (limited to 'etc/isar')
| -rw-r--r-- | etc/isar/XSymbolTests.thy | 15 |
1 files 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 |