doc-src/HOL/HOL-eg.txt
changeset 9269 b62d5265b959
parent 6580 ff2c3ffd38ee