This is perhaps slightly off-topic, but it relates to using OCaml's utop with some of John Harrison's code. It might have some degree of relevance to William Mitchell's recent request regarding HOL Light code.
A few months ago I put together a GitHub repository with some utilities and slightly modified versions of Harrison's sample code for his Handbook of Practical Logic and Automated Reasoning. The result runs with much more modern versions of OCaml compared with the original, and with utop if desired. Perhaps this would be of use in some way to some members of this list, though it is oriented toward first order logic. The repository is at https://github.com/crisperdue/practical-logic. Sorry, I have not tried to do anything similar for HOL Light. Best regards, -Cris
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
