From e0142f75d0c3e0061b65ed69b74351913c6aa0c9 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 26 May 2009 12:36:40 +0000
Subject: Test case for #266

---
 etc/isar/HighlightSize.thy | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 etc/isar/HighlightSize.thy

(limited to 'etc')

diff --git a/etc/isar/HighlightSize.thy b/etc/isar/HighlightSize.thy
new file mode 100644
index 00000000..386db167
--- /dev/null
+++ b/etc/isar/HighlightSize.thy
@@ -0,0 +1,13 @@
+(* See: http://proofgeneral.inf.ed.ac.uk/trac/ticket/266 *)
+
+theory HighlightSize imports Main
+begin
+
+lemmas rules = sym refl trans sym refl trans sym refl trans sym refl trans sym refl trans
+
+ML_command {* Pretty.writeln (Pretty.markup Markup.hilite
+  [ProofContext.pretty_fact @{context} ("foo", @{thms rules(1-14)})]) *}
+
+end
+
+
-- 
cgit v1.2.3