Thanks for this Michael.
I am using Ubuntu 14.10, Hol4 9, polyml 5.5.2, emacs 24.3.1 (the stock one
in Ubuntu), and in case it may also be helpful, I send you my .emacs file
(although is quite simple). Should I include anything else?
(add-to-list 'load-path "~/.emacs.d/")
(load "/home/david/Tools
Wow; I've never seen anything like this before.
Can you describe what setup you have please? What OS, what SML implementation
etc?
Thanks,
Michael
On 03/12/14 13:26, David Sanán wrote:
> Hi all,
> I recently changed my computer at home and reinstalled everything, including
> HOL4.But after the
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
whic
