doc-src/HOL/HOL-eg.txt
changeset 17186 797433ca1ab3
parent 6580 ff2c3ffd38ee