blob: 386db1673aea45035c7fb7aae954713fd9f31dba (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
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
|