diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 19:23:08 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 19:23:08 +0000 |
| commit | 548bc19c5e814be107a2f8e57872e0384174cb5c (patch) | |
| tree | e5b53708c3fb750bbcae4c0657ea4965a3649f7f /etc | |
| parent | 5b95560042dfb195abd925be4660011811e29684 (diff) | |
More tests
Diffstat (limited to 'etc')
| -rw-r--r-- | etc/isar/XSymbolTests.thy | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/etc/isar/XSymbolTests.thy b/etc/isar/XSymbolTests.thy index c1f2a976..1816e496 100644 --- a/etc/isar/XSymbolTests.thy +++ b/etc/isar/XSymbolTests.thy @@ -11,15 +11,18 @@ like \<alpha> doesn't immediately replace it. *) constdefs P1 :: bool ("P\<^sub>1") (* subscript *) "P\<^sub>1 == True" + P2 :: bool ("P\<^sup>2") (* superscript *) + "P\<^sup>2 == True" (* Buglet here: if we enable x-sym during scripting, - goals/response flks are not updated, so subscripts - do not appear in output windows. - Restarting prover fixes. + goals/response flks are not updated, so xsyms + do not appear in output windows. Stoping/starting + prover fixes. *) -theorem "P\<^sub>1"; (* check subscript appears in goals window *) -by (simp add: P1_def) (* .. and response window *) +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 *) |