diff options
| author | David Aspinall | 2008-01-15 23:45:30 +0000 |
|---|---|---|
| committer | David Aspinall | 2008-01-15 23:45:30 +0000 |
| commit | d59dbef33c35b3df1a197195ed186358cf211d2e (patch) | |
| tree | 78409c55ccc9a7603edeba7bca59b2f8302d23f4 /etc/isar/XSymbolTests.thy | |
| parent | 0d705351ce3aa6eb37384cce71d2d1aba1739229 (diff) | |
Updated.
Diffstat (limited to 'etc/isar/XSymbolTests.thy')
| -rw-r--r-- | etc/isar/XSymbolTests.thy | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/etc/isar/XSymbolTests.thy b/etc/isar/XSymbolTests.thy index 17fd88dd..3689f300 100644 --- a/etc/isar/XSymbolTests.thy +++ b/etc/isar/XSymbolTests.thy @@ -11,7 +11,9 @@ theory XSymbolTests imports Main begin (* Fri Dec 14 13:20:38 GMT 2007. http://proofgeneral.inf.ed.ac.uk/trac/ticket/161 Sub/superscript output not handled properly when enabled using - menu. *) + menu. Fix: add fontification to proof-x-symbol-decode-region, + fix in proof-x-symbol.el 8.10. +*) (* response output *) thm wf_trancl @@ -43,7 +45,7 @@ term "k\<^bsup>long\<^esup>" (* k black, long is blue *) lemma "A ==> A" . -- OK consts A :: bool -lemma "A ==> A" . -- "xsymbols shuld be displayed!" +lemma "A ==> A" . -- "xsymbols should be displayed!" (* Test electric token input: writing a token @@ -90,6 +92,8 @@ consts intof :: "nat \<Rightarrow> int" ("_\<^sub>\<int>" 50) mynat :: nat ("\<gamma>") +term "intof 3" + constdefs myint :: int "myint == \<gamma>\<^sub>\<int>" |