src/Pure/primitive_defs.ML
changeset 47602 3d44790b5ab0
parent 46218 ecf6375e2abb
child 56243 2e10a36b8d46