Re: [Hol-info] The origin of the HOL4 logo

I’m pretty sure I derived the small logo GIF file from the eps file in the HOL repo using some image manipulation process, and perhaps some bitmap tweaking. The photo may be the one linked to earlier at the URL under cl.cam.ac.uk/~mjcg. Michael On 19/12/17, 13:13, "Mario Castelán Castro" wr

Re: [Hol-info] The origin of the HOL4 logo

Thanks. This comment appears to refer to the old logo featured in the manual (because it was in the manual back when it featured that logo) instead of the current one (which is very similar). Do you have a link to the aforementioned photo of

Re: [Hol-info] The origin of the HOL4 logo

Our manuals’ acknowledgements text includes: The cover design is by Arnold Smith, who used a photograph of a `snow watching lantern' taken by Avra Cohn (in whose garden the original object resides). John Van Tassel composed the \LaTeX\ picture of the lantern. This would have been done

Re: [Hol-info] The origin of the HOL4 logo

On 14/12/17 12:00, Konrad Slind wrote: > Maybe you are thinking of the snow-watching latern? > > https://www.cl.cam.ac.uk/archive/mjcg/lantern.html Maybe. I am not sure, but I think not. This lantern is very similar to the older logo of HOL. I think that I recall seeing a photo that is almost i

Re: [Hol-info] The origin of the HOL4 logo

Maybe you are thinking of the snow-watching latern? https://www.cl.cam.ac.uk/archive/mjcg/lantern.html Konrad. On Thu, Dec 14, 2017 at 11:23 AM, Mario Castelán Castro < marioxcc...@yandex.com> wrote: > Hello. > > I recall having read that the HOL4 logo (as found in TUTORIAL, MANUAL, > DESCRIPT

[Hol-info] The origin of the HOL4 logo

Hello. I recall having read that the HOL4 logo (as found in TUTORIAL, MANUAL, DESCRIPTION, LOGIC) is based on a photo of a lamp found in Canada. Despite searching my browser history and using a search engine I failed to find the message again. To somebody who knows what photo I am referring to or