From 28555e28922c9f1478b7c8fac3cba6a425059eef Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 7 Mar 2003 12:24:22 +0000 Subject: Remove notes about old bugs --- etc/isar/XSymbolTests.thy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'etc/isar') 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 \ P\<^sup>2"; (* check fonts in goals window *) by (simp add: P1_def P2_def) (* .. and response window *) -(* BUG: \ not appearing in response *) consts "P\<^sup>\" :: bool (* superscript of a token char *) @@ -39,7 +38,7 @@ consts (* Markus reports that \ 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 \. 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 -- cgit v1.2.3