diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-08-28 14:35:00 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-28 14:35:00 +0000 |
| commit | ecd67cfbf3df2623d251d4b60529e7293051852b (patch) | |
| tree | 144c841d743ecea76e133fa26a93347895a1de07 /etc | |
| parent | b1b239a703855b3a603f48683413d0e709483ddd (diff) | |
Exercise bug in pg-remove-specials breaking x-sym display in Isabelle
Diffstat (limited to 'etc')
| -rw-r--r-- | etc/isar/XSymbolTests.thy | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/etc/isar/XSymbolTests.thy b/etc/isar/XSymbolTests.thy index 1816e496..6be971e2 100644 --- a/etc/isar/XSymbolTests.thy +++ b/etc/isar/XSymbolTests.thy @@ -4,9 +4,18 @@ theory XSymbolTests = Main: -(* At the moment, electric token input doesn't work -despite being enabled. So writing a token -like \<alpha> doesn't immediately replace it. *) + +(* 28.8.02: bug in pg-remove-specials broke this; now fixed *) + +lemma "A ==> A" . -- OK + +consts A :: bool +lemma "A ==> A" . -- "xsymbols not displayed?" + + +(* Test electric token input: writing a token +like \ <alpha> (without space, \<alpha>) should immediately +replace it. *) constdefs P1 :: bool ("P\<^sub>1") (* subscript *) @@ -29,7 +38,7 @@ consts "\<^bold>X" :: bool (* bold character *) -(* Markus reports that · is saved in the file as +(* 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. *) |