rebuilt from fresh copy of Bitstream Vera, for improved quality of regular text glyphs;
misc cleanup of mathematical glyphs, with bold version synthesized by fontforge;
(benchmark Isabelle
:extrasorts ( T1 T2)
:extrafuns (
(uf_2 T1)
(uf_3 T1)
)
:extrapreds (
(up_1 T1)
)
:assumption (if_then_else (up_1 uf_2) (not (exists (?x1 T1) (up_1 ?x1))) (forall (?x2 T1) (not (up_1 ?x2))))
:assumption (not (implies (up_1 uf_2) (up_1 uf_3)))
:formula true
)