src/Pure/primitive_defs.ML
changeset 83417 b51e4a526897
parent 81545 6f8a56a6b391