navigation / documentation overview / developer documentation / proof assistant comparison
Recommendation: Read the user documentation and FAQ first. This page assumes familiarity with the jargon used in the Physics Derivation Graph.
HOL Light tutorial