blob: 7c68b74fbd2f0b99d266ed5734491e42013fbc42 (
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
[Proof_Context.pretty_fact @{context} ("foo", @{thms rules(1-14)})]) *}
end
|
