Create HOL.gitignore

[lorenzleutgeb]

Reasons

Making it easier to get started with HOL.

Support

• The .gitignore of the HOL repository itself.
• The .gitignore of CakeML, a large project implemented in HOL.
• Section 8.3 in The HOL System Description.
• A private conversation with long-time maintainer @mn200 confirming that the change represents a reasonable default.

About

Quoting from hol-theorem-prover.org:

What is HOL?
The HOL interactive theorem prover is a proof assistant for higher-order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems (users may have to prove the hard theorems themselves!) An oracle mechanism gives access to external programs such as SMT and BDD engines. HOL is particularly suitable as a platform for implementing combinations of deduction, execution and property checking.

History
During the last 30 years there have been several widely used versions of the HOL system:

1. HOL88 from Cambridge;
2. HOL90 from Calgary and Bell Labs;
3. HOL98 from Cambridge, Glasgow and Utah.