guide me towards this theorem?
Best regards,
Elif Deniz
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
eport what you get when you do a
M-x emacs-version
so I can try to adjust the elisp code to cope with older versions?
Alternatively, try
sudo apt install emacs26
Best wishes,
Michael
On 17/3/21, 09:17, "Elif Deniz" wrote:
Dear all,
I have a problem while using emacs after
Dear all,
I have a problem while using emacs after installation HOL4 as following:
"Symbol's function definition is void: if let*"
When I want to run HOL4 (polyml5.7.1 or polyml5.8.1, kananaskis-13 or
kananaskis-14) on Ubuntu 16 or Ubuntu 18 which is already all
correctly installed. But, w
Hi Petros,
Thank you for your response. Yes, it is warning and seems like running.
But, when I want to load "Multivariate/realanalysis.ml" or "Multivariate/
cauchy.ml" theories; after loading almost 45 minutes, system killed and I
couldn't load these theories. So, I thought maybe it is not proper
Dear all,
I'm trying to install HOL-Light on Ubuntu 14.04 and following the
instruction on Github website. When I do #use "hol.ml" on ocaml interface,
I'm facing the following errors:
File "/home/elif/hol-light/impconv.ml" , line 315, characters 8-174:
Warning 8: this pattern-matching is not exha
