We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see ourdocumentation.
There was an error while loading.Please reload this page.
1 parent2664fdf commita430bc0Copy full SHA for a430bc0
index.md
@@ -79,5 +79,14 @@ This website gives a brief overview of our [HOLMS library](https://github.com/HO
79
- Leonardo Quartini, University of Florence, Italy
80
81
82
-##HOLMSUSAGE GUIDE
+##HOLMSUsage Guide
83
The[README.md](https://github.com/HOLMS-lib/HOLMS/blob/main/README.md) provides a usage guide for our HOLMS library at its current status.
84
+
85
86
+##HOL Light Mini-Manual
87
88
+A 30-page**introductory guide for non-specialists**, taken from Chapter 2 of[Antonella Bilotta’s Master’s Thesis](https://arxiv.org/abs/2506.10048).
89
+Useful for students, researchers, and contributors approaching**mechanisation in HOL Light** or in a**proof assistant** for the first time.
90
91
+[Read the Mini-Manual (PDF, arXiv)](https://arxiv.org/pdf/2506.10048.pdf#page=68)
92