From 5db7de75e8f88750844bf438a9bfbe0e52a8dc41 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 14 Dec 2007 14:39:22 +0000
Subject: Updated.

---
 etc/isar/XSymbolTests.thy | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/etc/isar/XSymbolTests.thy b/etc/isar/XSymbolTests.thy
index b03edfe5..17fd88dd 100644
--- a/etc/isar/XSymbolTests.thy
+++ b/etc/isar/XSymbolTests.thy
@@ -6,7 +6,19 @@
    $Id$
 *)
 
-theory XSymbolTests = Main:
+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. *)
+
+(* response output *)
+thm wf_trancl
+
+(* goals output *)
+lemma wf_trancl2 : "wf ?r \<Longrightarrow> wf (?r\<^sup>+)"
+by auto
 
 (* Thu Sep 25 16:26:47 BST 2003.  
    Problem reported by Norbert Schirmer <norbert.schirmer@web.de>
-- 
cgit v1.2.3