概要

チュートリアルとドキュメント

ゼロから始めて、HOLを使いこなせるようになるには平均で1ヶ月ほどかかります。Emacsのユーザには、HOLの使い方とEmacsを使った基本的な証明の11ページにわたるガイドがあります。Emacsモードのより完全なドキュメントのページもあります。VimユーザーはVimプラグインのドキュメントを参照するとよいでしょう。

新しい人のためのもう一つの良いリソースはチュートリアルです。それは新しいユーザーのためのシステムの紹介と、詳細なインストール手順を提供します。 このコースはPROSPERプロジェクトのニーズを狙い、HOLの実地体験を提供しようとしたものです。 スライド（印刷用、LaTeXソース）と演習シートが公開されています。 また、トラブルシューティングのためのFAQも用意されています。

詳細なドキュメント

説明マニュアルはHOLの全ての機能を詳細に説明しています。これは高レベルのライブラリだけでなく、HOL APIにおけるMLのコア機能のいくつかを含みます。 このページのローカルコピーは、HOLをインストールしたときに構築されることに注意してください。 このページは HOL/help/HOLindex.html にあり、HOL は HOL のインストール先のルートです。

論理マニュアル(イタリア語版もあります)は、HOLで実装されている高階論理の詳細な数学的記述を提供しています。 特に、ZFC集合論における論理とその定義原理のモデルを示しています

。