From d59dbef33c35b3df1a197195ed186358cf211d2e Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 15 Jan 2008 23:45:30 +0000
Subject: Updated.

---
 etc/isar/XSymbolTests.thy | 8 ++++++--
 1 file 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>"
-- 
cgit v1.2.3