doc-src/HOL/HOL-eg.txt
changeset 39260 f94c53d9b8fb
parent 6580 ff2c3ffd38ee
equal deleted inserted replaced
39259:194014eb4f9f 39260:f94c53d9b8fb