1 files changed, 13 insertions, 0 deletions
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
+
+