doc-src/IsarRef/hol.tex
changeset 9780 d25d6a977ea6
parent 9751 1287787744a7
child 9800 221388d5696d