diff options
| author | David Aspinall | 2003-09-25 15:46:12 +0000 |
|---|---|---|
| committer | David Aspinall | 2003-09-25 15:46:12 +0000 |
| commit | e73de67a758e71ee4fb69397cb538c62c7b4fe92 (patch) | |
| tree | f70a941c18e6c1a9ca5bffc30b47566d06056097 | |
| parent | 175073bbd8d084256226ea22267cae142f3a387b (diff) | |
Add bug reported by Norbert Schirmer.
[Actually, superscript highlighting seems broken anyway]
| -rw-r--r-- | etc/isar/XSymbolTests.thy | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/etc/isar/XSymbolTests.thy b/etc/isar/XSymbolTests.thy index 09952ecd..73c90e75 100644 --- a/etc/isar/XSymbolTests.thy +++ b/etc/isar/XSymbolTests.thy @@ -4,6 +4,18 @@ theory XSymbolTests = Main: +(* Thu Sep 25 16:26:47 BST 2030. + Problem reported by Norbert Schirmer <norbert.schirmer@web.de> + Currently, superscript output highlighting seems broken anyway? *) + +consts silly:: "'a => 'a => 'a" ("_\<^sup>_" [1000,1000] 1000) + +consts k:: 'a + +term "a\<^sup>b" (* b should be a blue variable *) +term "a\<^sup>k" (* k should be a black constant *) + + (* 28.8.02: bug in pg-remove-specials broke this; now fixed *) @@ -42,7 +54,7 @@ consts x-symbol-invisitiblity-spec type error, at least during editing. *) consts - intof :: nat \<Rightarrow> int ("_\<^sub>\<int>" 50) + intof :: "nat \<Rightarrow> int" ("_\<^sub>\<int>" 50) mynat :: nat ("\<gamma>") constdefs |