aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/isar/XSymbolTests.thy
diff options
context:
space:
mode:
Diffstat (limited to 'etc/isar/XSymbolTests.thy')
-rw-r--r--etc/isar/XSymbolTests.thy14
1 files changed, 13 insertions, 1 deletions
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>