diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-03-07 12:24:22 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-03-07 12:24:22 +0000 |
| commit | 28555e28922c9f1478b7c8fac3cba6a425059eef (patch) | |
| tree | a5cb8ca7ea25180ce34c5522932d5029d41926ed /etc/isar/XSymbolTests.thy | |
| parent | 28ec25e93a1c15f7e0caec83285d800435750459 (diff) | |
Remove notes about old bugs
Diffstat (limited to 'etc/isar/XSymbolTests.thy')
| -rw-r--r-- | etc/isar/XSymbolTests.thy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/etc/isar/XSymbolTests.thy b/etc/isar/XSymbolTests.thy index 6be971e2..9095555c 100644 --- a/etc/isar/XSymbolTests.thy +++ b/etc/isar/XSymbolTests.thy @@ -31,7 +31,6 @@ constdefs theorem "P\<^sub>1 \<and> P\<^sup>2"; (* check fonts in goals window *) by (simp add: P1_def P2_def) (* .. and response window *) -(* BUG: \<and> not appearing in response *) consts "P\<^sup>\<alpha>" :: bool (* superscript of a token char *) @@ -39,7 +38,7 @@ consts (* Markus reports that \<cdot> is saved in the file as -an 8-bit character. I can't repeat that with XEmacs 21.4, + an 8-bit character. I can't repeat that with XEmacs 21.4, unless I set the relevant X-Symbol menu option. *) (* @@ -48,7 +47,8 @@ unless I set the relevant X-Symbol menu option. *) for \<circ>. But subsequent buffers to be visited work fine. Problem is stable for turning x-symbol on/off. Revisting the first buffer cures the problem. - I can't easily repeat the problem... + Update: May be inherent problem with non-Mule version of + X-Symbol (CW suggests) *) consts |