The files here are part of joint project between Mike Gordon
(University of Cambridge) and Warren Hunt and Matt Kaufmann
(University of Texas) to develop a logically sound and robust link
between the HOL4 and ACL2 proof tools.

This is work in progress. For pending issues, see ISSUES in this
directory.

The files and directories here are:

.acl2holrc.bash ............... See below
README ........................ This file
ISSUES ........................ Implementation topics, pending work, bugfixes
ml ............................ ML and HOL files
lisp .......................... Lisp and ACL2 files
examples ...................... Various examples and case studies
tests ......................... Regression tests
use-cases.txt ................. Some use cases with discussion of trust issues

To use these tools, edit the following file to give correct paths:

  .acl2holrc.bash

You don't have to do anything further with this file, as it is
automatically "source"d in the top-level test script, tests/doit.
However, you may wish to execute

  source .acl2holrc.bash

in your bash shell, in case you are using tools in any way other than
through tests/doit.

-----------------------------------------------------------------
An unpublished paper written in 2006 by Gordon, Hunt and Kaufmann
entitled "Connecting HOL to ACL2" can be found at
http://www.cl.cam.ac.uk/users/mjcg/hol2acl2/papers/HOL-ACL2-V2.4.pdf.
There is also website associated with this paper:
http://www.cl.cam.ac.uk/~mjcg/hol2acl2/backpack/GordonHuntKaufmannPaper.html.
-----------------------------------------------------------------

Originally created by Mike Gordon (16 Dec, 2005)
Updated by Matt Kaufmann (8 Dec, 2008; 19 Aug, 2010)
Updated by Mike Gordon and Matt Kaufmann (9 Sep, 2010)
Updated by Mike Gordon (14 Nov, 2016)