src/Pure/defs.ML
changeset 32804 ca430e6aee1c
parent 32050 ebb9274e34b7
child 32785 ec5292653aff