diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-02 18:10:12 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-02 18:10:12 +0000 |
| commit | b40411049f0f407b40c78596f03ec960e4d7389b (patch) | |
| tree | fcb0fab471cace8b2c484e09f1325dd81e6ed44e /etc/isar/XSymbolTests.thy | |
| parent | 64ca4589193fcfb0615275dd1f5dd78e31d45cc8 (diff) | |
Add test of spanning sup/sub
Diffstat (limited to 'etc/isar/XSymbolTests.thy')
| -rw-r--r-- | etc/isar/XSymbolTests.thy | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/etc/isar/XSymbolTests.thy b/etc/isar/XSymbolTests.thy index 73c90e75..2b4ea117 100644 --- a/etc/isar/XSymbolTests.thy +++ b/etc/isar/XSymbolTests.thy @@ -41,12 +41,19 @@ constdefs prover fixes. *) +constdefs (* long sub/sups, new 29/12/03, added by Gerwin Klein *) + + Plow :: bool ("P\<^bsub>low\<^esub>") (* spanning subscript *) + Phigh :: bool ("P\<^bsup>high\<^esup>") (* spanning superscript *) + + theorem "P\<^sub>1 \<and> P\<^sup>2"; (* check fonts in goals window *) by (simp add: P1_def P2_def) (* .. and response window *) consts "P\<^sup>\<alpha>" :: bool (* superscript of a token char *) - "\<^bold>X" :: bool (* bold character *) + "\<^bold>X" :: bool (* bold character + [not supported in current X-Symbols] *) (* test: using a symbol as a subscript *) |