Re: [Hol-info] Difference between sets formats

the > paired abstraction > is an unspecified function of the structure of t (it is approximately left > to right). > > I hope this helps. > > Thomas > > > On 25.10.19 18:05, Yassmeen Derhalli wrote: > > Hi, > I have this proof goal, where I need to prove t

[Hol-info] Difference between sets formats

Hi, I have this proof goal, where I need to prove that two sets are equal. {{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} | a | a IN if j IN L then s3 j else s4 j} = {{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} | a IN if j IN L then s3 j

Re: [Hol-info] Exception raised while using HOL in hol-mode

ner, I had the problem before that the > communication with HOL worked just fine, but HOL and emacs saw different > "/tmp" directories (e.g. the ones on the local and remote machine). Are you > using anything like this? What environment are you running HOL in? > > Best > &

[Hol-info] Exception raised while using HOL in hol-mode

Hi, Sorry for sending this email again, but it seems that there was a problem with the first email I am using HOL4, yesterday I started receiving this error message Exception raised Io {cause = SysErr ("No such file or directory", SOME ENOENT), function = "TextIO.openIn", name =

[Hol-info] (no subject)

Hi, I am using HOL4 in hol-mode, yesterday I started receiving this error message ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info