Michael thanks a lot.
I was using it with HO_MATCH_MP_TAC ITSET_IND
GEN_ALL helped! I didn't thought on that... my fault!
offtopic,
Always I send I message to the mailing list I get moderator approval
message, although I signed up to HOL4 mailing list with this email address.
Is this the normal b
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
Call for Workshop Proposals
CICM 2015 - Conference on Intelligent Computer Mathematics
July 13-17, 2015
The George Washington University, Washington, D.C ,
On 03/12/14 13:19, David Sanán wrote:
> offtopic, Always I send I message to the mailing list I get
> moderator approval message, although I signed up to HOL4 mailing
> list with this email address. Is this the normal behaviour???
> Thanks!
At the moment, this is normal for new posters, whether o
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
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
