From 548bc19c5e814be107a2f8e57872e0384174cb5c Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 18 Jul 2002 19:23:08 +0000 Subject: More tests --- etc/isar/XSymbolTests.thy | 13 ++++++++----- 1 file 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 \ 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 \ 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 *) -- cgit v1.2.3