doc-src/HOL/HOL-eg.txt
changeset 26619 c348bbe7c87d
parent 6580 ff2c3ffd38ee