diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-02 18:16:09 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-02 18:16:09 +0000 |
| commit | fac372ba7f578e8ba5022b0050da51bd1dd07279 (patch) | |
| tree | 6689d5d75af971bd70d6909bcdab4d8c6aa45499 /etc | |
| parent | b40411049f0f407b40c78596f03ec960e4d7389b (diff) | |
More comments/test printing.
Diffstat (limited to 'etc')
| -rw-r--r-- | etc/isar/XSymbolTests.thy | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/etc/isar/XSymbolTests.thy b/etc/isar/XSymbolTests.thy index 2b4ea117..3b5ccf00 100644 --- a/etc/isar/XSymbolTests.thy +++ b/etc/isar/XSymbolTests.thy @@ -1,4 +1,8 @@ (* Some checks for X-Symbol behaviour. + + This file should be displayed sensibly, and also the + display back from Isabelle ought to match. + $Id$ *) @@ -22,7 +26,7 @@ term "a\<^sup>k" (* k should be a black constant *) lemma "A ==> A" . -- OK consts A :: bool -lemma "A ==> A" . -- "xsymbols not displayed?" +lemma "A ==> A" . -- "xsymbols shuld be displayed!" (* Test electric token input: writing a token @@ -41,11 +45,16 @@ constdefs prover fixes. *) +thm P1_def P2_def (* check display from Isabelle *) + constdefs (* long sub/sups, new 29/12/03, added by Gerwin Klein *) Plow :: bool ("P\<^bsub>low\<^esub>") (* spanning subscript *) + "P\<^bsub>low\<^esub> \<equiv> True" Phigh :: bool ("P\<^bsup>high\<^esup>") (* spanning superscript *) + "P\<^bsup>high\<^esup> \<equiv> True" +thm Plow_def Phigh_def (* check display from Isabelle *) theorem "P\<^sub>1 \<and> P\<^sup>2"; (* check fonts in goals window *) by (simp add: P1_def P2_def) (* .. and response window *) |