doc-src/HOL/HOL.tex
changeset 12326 b4e706774e96
parent 12180 91c9f661b183
child 12611 c44a9fecb518