Hi all,
I recently changed my computer at home and reinstalled everything,
including HOL4.But after the reinstall HOL output shows double empty lines,
e.g.
ITSET_IND;
val it =
|- ∀P.
(∀s b. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s) (f (CHOICE s) b)) ⇒ P s b) ⇒
∀v v1. P v v1:
thm
which is a little bit annoying for me...
is it possible to adjust this somehow?
Many thanks,
David.
------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
